Theorem mp3an 1378

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 1365	. 2 |- ( ( ps /\ ch ) -> th )
6	1, 2, 5	mp2an 430	1 |- th

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  vtocl3  2879  raltp  3766  rextp  3767  ordtriexmidlem  4666  ordtri2or2exmidlem  4673  onsucelsucexmidlem  4676  ordsoexmid  4709  funopg  5411  ftp  5900  caovass  6250  caovdi  6269  mptexw  6342  ofmres  6369  mpofvexi  6442  mpoexw  6449  dmtpos  6527  rntpos  6528  dftpos3  6533  tpostpos  6535  mapsnen  7100  xpcomen  7125  mapxpen  7148  xpmapenlem  7149  unfiexmid  7225  1lt2pi  7708  1lt2nq  7774  halfnqq  7778  m1p1sr  8128  m1m1sr  8129  suplocsrlempr  8175  addassi  8335  mulassi  8336  adddii  8337  adddiri  8338  lttri  8432  lelttri  8433  ltletri  8434  letri  8435  mul12i  8474  mul32i  8475  add12i  8491  add32i  8492  addcani  8510  addcan2i  8511  subaddi  8615  subadd2i  8616  subsub23i  8618  addsubassi  8619  addsubi  8620  subcani  8621  subcan2i  8622  pnncani  8623  subdii  8736  subdiri  8737  ltadd2i  8750  ltadd1i  8832  leadd1i  8833  leadd2i  8834  ltsubaddi  8835  lesubaddi  8836  ltsubadd2i  8837  lesubadd2i  8838  ltaddsubi  8839  gtapii  8965  mulcanapi  8998  divclapi  9087  divcanap2i  9088  divcanap1i  9089  divrecapi  9090  divcanap3i  9091  divcanap4i  9092  divassapi  9101  divdirapi  9102  div23api  9103  div11api  9104  sup3exmid  9290  1mhlfehlf  9528  halfpm6th  9530  3halfnz  9748  addex  10063  mulex  10064  unirnioo  10386  nnenom  10886  inftonninf  10894  m1expcl2  11013  i4  11094  expnass  11097  bcn1  11212  hashinfom  11233  abs3difi  11939  0.999...  12307  ef01bndlem  12542  cos1bnd  12545  cos2bnd  12546  sin4lt0  12553  3dvdsdec  12651  3dvds2dec  12652  ndvdsi  12719  flodddiv4  12722  3lcm2e6woprm  12883  6lcm4e12  12884  3prm  12925  dec2dvds  13213  modxai  13218  gcdi  13223  numexp2x  13228  2exp5  13235  2exp11  13239  ballotfilem2  13280  ballotfilemafi  13290  ballotfilembfi  13291  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemth  13333  znnen  13341  ennnfonelem1  13350  prminf  13398  topnfn  13651  prdsvallem  13674  prdsval  14264  fnmgp  14310  rhmex  14555  rmodislmodlem  14778  rmodislmod  14779  cnfldstr  14986  zring0  15026  fnpsr  15142  mplvalcoe  15180  fnmpl  15183  xmetunirn  15558  tgioo  15754  tgqioo  15755  addcncntoplem  15761  expcncf  15809  dveflem  15926  dvef  15927  efcn  15968  sinhalfpilem  15992  sincosq1lem  16026  sincosq4sgn  16030  cosq23lt0  16034  coseq00topi  16036  coseq0negpitopi  16037  tangtx  16039  sincos4thpi  16041  sincos6thpi  16043  pigt3  16045  cos02pilt1  16053  cos0pilt1  16054  2logb9irr  16181  2logb3irr  16183  2logb9irrALT  16184  sqrt2cxp2logb9e3  16185  2irrexpq  16186  2logb9irrap  16187  2irrexpqap  16188  log2tlbndlog2  16194  log2ublem1  16195  log2ublem2  16196  log2ublog2  16198  1sgm2ppw  16263  ppiqub  16267  bclbnd  16281  bposlem8  16292  lgseisenlem1  16368  lgseisenlem2  16369  lgsquadlem1  16375  upgr2wlkdc  16797  konigsberglem1  16908  konigsberglem2  16909  konigsberglem3  16910  konigsberglem5  16912  ex-fl  16918  ex-exp  16920  repiecelem  17253  repiecege0  17255  trilpolemeq1  17269