Theorem mp3an 1327

Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.)

Hypotheses

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

Assertion

Ref	Expression
mp3an	|- th

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 |- ps
2		mp3an.3	. 2 |- ch
3		mp3an.1	. . 3 |- ph
4		mp3an.4	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
5	3, 4	mp3an1 1314	. 2 |- ( ( ps /\ ch ) -> th )
6	1, 2, 5	mp2an 423	1 |- th

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  vtocl3  2782  raltp  3633  rextp  3634  ordtriexmidlem  4496  ordtri2or2exmidlem  4503  onsucelsucexmidlem  4506  ordsoexmid  4539  funopg  5222  ftp  5670  caovass  6002  caovdi  6021  mptexw  6081  ofmres  6104  mpofvexi  6174  mpoexw  6181  dmtpos  6224  rntpos  6225  dftpos3  6230  tpostpos  6232  mapsnen  6777  xpcomen  6793  mapxpen  6814  xpmapenlem  6815  unfiexmid  6883  1lt2pi  7281  1lt2nq  7347  halfnqq  7351  m1p1sr  7701  m1m1sr  7702  suplocsrlempr  7748  addassi  7907  mulassi  7908  adddii  7909  adddiri  7910  lttri  8003  lelttri  8004  ltletri  8005  letri  8006  mul12i  8044  mul32i  8045  add12i  8061  add32i  8062  addcani  8080  addcan2i  8081  subaddi  8185  subadd2i  8186  subsub23i  8188  addsubassi  8189  addsubi  8190  subcani  8191  subcan2i  8192  pnncani  8193  subdii  8305  subdiri  8306  ltadd2i  8318  ltadd1i  8400  leadd1i  8401  leadd2i  8402  ltsubaddi  8403  lesubaddi  8404  ltsubadd2i  8405  lesubadd2i  8406  ltaddsubi  8407  gtapii  8532  mulcanapi  8564  divclapi  8650  divcanap2i  8651  divcanap1i  8652  divrecapi  8653  divcanap3i  8654  divcanap4i  8655  divassapi  8664  divdirapi  8665  div23api  8666  div11api  8667  sup3exmid  8852  1mhlfehlf  9075  halfpm6th  9077  3halfnz  9288  unirnioo  9909  nnenom  10369  inftonninf  10376  m1expcl2  10477  i4  10557  expnass  10560  bcn1  10671  hashinfom  10691  abs3difi  11098  0.999...  11462  ef01bndlem  11697  cos1bnd  11700  cos2bnd  11701  sin4lt0  11707  3dvdsdec  11802  3dvds2dec  11803  ndvdsi  11870  flodddiv4  11871  3lcm2e6woprm  12018  6lcm4e12  12019  3prm  12060  znnen  12331  ennnfonelem1  12340  prminf  12388  topnfn  12561  xmetunirn  12998  tgioo  13186  tgqioo  13187  addcncntoplem  13191  expcncf  13232  dveflem  13327  dvef  13328  efcn  13329  sinhalfpilem  13352  sincosq1lem  13386  sincosq4sgn  13390  cosq23lt0  13394  coseq00topi  13396  coseq0negpitopi  13397  tangtx  13399  sincos4thpi  13401  sincos6thpi  13403  pigt3  13405  cos02pilt1  13412  cos0pilt1  13413  2logb9irr  13529  2logb3irr  13531  2logb9irrALT  13532  sqrt2cxp2logb9e3  13533  2irrexpq  13534  2logb9irrap  13535  2irrexpqap  13536  ex-fl  13606  ex-exp  13608  trilpolemeq1  13919