Theorem mp3an1 900

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3an1.1	|- ph
mp3an1.2	|- ((ph /\ ps /\ ch) -> th)

Assertion

Ref	Expression
mp3an1	|- ((ps /\ ch) -> th)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 |- ph
2		mp3an1.2	. . 3 |- ((ph /\ ps /\ ch) -> th)
3	2	3expb 832	. 2 |- ((ph /\ (ps /\ ch)) -> th)
4	1, 3	mpan 693	1 |- ((ps /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773

This theorem is referenced by:  mp3an12 903  mp3an1i 906  mp3anl1 907  mp3an 913  onint 2996  tfrlem9 3904  oaord1 4169  oaword2 4171  oawordeulem 4172  oa00 4177  omword1 4188  omword2 4189  omlimcl 4193  unfilem2 4525  fodomb 4772  brdom3 4773  brdom7disj 4776  brdom6disj 4777  mulclpi 4993  mulidpq 5041  halfpq 5054  cnegext 5320  negeu 5327  muladd11t 5394  xrre2t 5543  ltaddpost 5624  addge01t 5645  receu 5670  recclt 5684  div0t 5723  recdiv2t 5752  rerecclt 5759  ltmul12it 5797  lemul12itOLD 5799  lemul12it 5800  mulgt1t 5801  lediv12it 5844  ledivp1t 5853  nngt1ne1t 5892  nnaddm1clt 5905  8th4div3 5978  infm3 6001  infmrcl 6016  xrub 6027  supxrre 6030  nn0ltp1let 6074  gtndivt 6140  nn0ind 6160  qbtwnxr 6217  qsqueeze 6218  om2uzran 6237  ser1mono 6274  elioc2t 6322  elico2t 6323  elicc2t 6324  elfz2nn0t 6427  expubndt 6539  le2sqit 6563  bernneq 6583  sqr2irr 6659  imret 6710  cau4i 6855  cau5 6856  cvg3 6860  faclbnd5 6890  fsumcom 6966  climubi 7089  climsup 7091  caucvglem6 7098  caucvg 7099  serzf0 7105  cvgcmp 7120  cvgcmpub 7121  isumnn0nn 7142  geoser 7169  georeclim 7175  geoisumr 7178  0.999... 7181  cvgratlem4 7188  efcltlem1 7246  erelem3 7263  efaddlem6 7285  efaddlem15 7294  ef01tllem2 7326  effsumle 7338  efi4pt 7377  cos2tt 7405  sin01bndlem3 7411  cos01bndlem3 7413  sin01gt0 7418  cos01gt0 7419  demoivre 7426  znnen 7445  infpn2 7452  iooretop 7601  metxplem1 7766  metxplem2 7767  metxplem3 7768  metxp 7774  bl2in 7783  methausi 7820  xplmi 7907  xpcn 7910  bcthlem3 7935  bcthlem9 7941  bcthlem20 7952  bcthlem21 7953  bcthlem24 7956  bcthlem25 7957  isgrpi 7976  ghgrpilem3 8072  ghgrpilem4 8073  ghsubgi 8075  imsmetlem 8261  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  ipval2 8291  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem5 8311  ip1cnilem6 8312  lnocoi 8352  nmlno0lem 8385  nmblolbii 8390  blometi 8394  blocnilem 8395  blocni 8396  ipasslem1 8421  ipasslem2 8422  ipasslem4 8424  ipasslem5 8425  ipasslem8 8428  ipblnfi 8447  ip2eqi 8448  ubthlem6 8465  ubthlem7 8466  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  ubthlem14 8473  minveclem9 8484  minveclem15 8490  minveclem16 8491  minveclem18 8493  minveclem19 8494  minveclem21 8496  minveclem25 8500  minveclem27 8502  minveclem28 8503  minveclem30 8505  minveclem31 8506  minveclem35 8510  minveclem36 8511  minveclem37 8512  minveclem38 8513  minveceu 8514  htthlem6 8555  htthlem10 8559  sincosq1eq 8626  efghgrpilem 8634  efifolem5 8641  shftefif1olem 8661  shftefif1olemOLD 8662  logeftb 8686  logeftbOLD 8706  h2hmetdval 8787  hvm1negt 8822  hvsub4t 8827  hvsubdistr2t 8838  hv2timest 8849  hvsubcant 8862  hvsubcan2t 8863  his2subt 8879  his6t 8886  norm-it 8917  normpyct 8934  hhip 8965  hhph 8966  hhcms 8993  hhssabl 9053  hhssnv 9054  hhshsslem2 9058  hhssmetdval 9066  hhsscms 9067  projlem26 9127  projlem30 9131  shscl 9196  shunss 9252  h1datom 9421  osumlem6 9500  homulid2t 9643  honegdit 9652  ho2timest 9662  nmopge0t 9751  nmopgt0t 9752  nmfnge0t 9767  lnopadd 9811  lnopmul 9812  lnopsub 9814  hmopbdopHIL 9828  nmbdoplb 9864  nmcoplb 9873  nmophm 9876  lnopcon 9878  lnfnadd 9887  lnfnsub 9890  nmbdfnlb 9893  nmcfnlb 9902  lnfncon 9905  cnlnadjlem2 9916  cnlnadjlem7 9921  adjbdlnt 9931  nmoptri 9941  nmopco 9942  adjco 9947  nmopcoadj 9948  leopmult 9979  hmopidmchlem 9989  hmopidmpj 9991  pjima 10015  sto2 10074  atcveq0 10183  atcv0eq 10214  atoml 10217  atcvat 10221  atcvat3 10231  ghomgrpilem2 10291  ghomsn 10293  cayleylem2 10317

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775

Copyright terms: Public domain