Theorem mp3an 1378

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

Hypotheses

Ref	Expression
mp3an.1	⊢ 𝜑
mp3an.2	⊢ 𝜓
mp3an.3	⊢ 𝜒
mp3an.4	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an	⊢ 𝜃

Proof of Theorem mp3an

Step	Hyp	Ref	Expression
1		mp3an.2	. 2 ⊢ 𝜓
2		mp3an.3	. 2 ⊢ 𝜒
3		mp3an.1	. . 3 ⊢ 𝜑
4		mp3an.4	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
5	3, 4	mp3an1 1365	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 430	1 ⊢ 𝜃

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  14257  fnmgp  14303  rhmex  14548  rmodislmodlem  14771  rmodislmod  14772  cnfldstr  14979  zring0  15019  fnpsr  15135  mplvalcoe  15172  fnmpl  15175  xmetunirn  15550  tgioo  15746  tgqioo  15747  addcncntoplem  15753  expcncf  15801  dveflem  15918  dvef  15919  efcn  15960  sinhalfpilem  15984  sincosq1lem  16018  sincosq4sgn  16022  cosq23lt0  16026  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  pigt3  16037  cos02pilt1  16044  cos0pilt1  16045  2logb9irr  16168  2logb3irr  16170  2logb9irrALT  16171  sqrt2cxp2logb9e3  16172  2irrexpq  16173  2logb9irrap  16174  2irrexpqap  16175  log2tlbndlog2  16181  log2ublem1  16182  log2ublem2  16183  log2ublog2  16185  1sgm2ppw  16250  ppiqub  16254  bclbnd  16268  bposlem8  16279  lgseisenlem1  16355  lgseisenlem2  16356  lgsquadlem1  16362  upgr2wlkdc  16784  konigsberglem1  16895  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  ex-fl  16905  ex-exp  16907  repiecelem  17240  repiecege0  17242  trilpolemeq1  17256