Theorem mp3an 1371

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 1358	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
6	1, 2, 5	mp2an 426	1 ⊢ 𝜃

Syntax hints:   → wi 4   ∧ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  vtocl3  2858  raltp  3724  rextp  3725  ordtriexmidlem  4615  ordtri2or2exmidlem  4622  onsucelsucexmidlem  4625  ordsoexmid  4658  funopg  5358  ftp  5834  caovass  6178  caovdi  6197  mptexw  6270  ofmres  6293  mpofvexi  6366  mpoexw  6373  dmtpos  6417  rntpos  6418  dftpos3  6423  tpostpos  6425  mapsnen  6981  xpcomen  7006  mapxpen  7029  xpmapenlem  7030  unfiexmid  7103  1lt2pi  7550  1lt2nq  7616  halfnqq  7620  m1p1sr  7970  m1m1sr  7971  suplocsrlempr  8017  addassi  8177  mulassi  8178  adddii  8179  adddiri  8180  lttri  8274  lelttri  8275  ltletri  8276  letri  8277  mul12i  8315  mul32i  8316  add12i  8332  add32i  8333  addcani  8351  addcan2i  8352  subaddi  8456  subadd2i  8457  subsub23i  8459  addsubassi  8460  addsubi  8461  subcani  8462  subcan2i  8463  pnncani  8464  subdii  8576  subdiri  8577  ltadd2i  8590  ltadd1i  8672  leadd1i  8673  leadd2i  8674  ltsubaddi  8675  lesubaddi  8676  ltsubadd2i  8677  lesubadd2i  8678  ltaddsubi  8679  gtapii  8804  mulcanapi  8837  divclapi  8924  divcanap2i  8925  divcanap1i  8926  divrecapi  8927  divcanap3i  8928  divcanap4i  8929  divassapi  8938  divdirapi  8939  div23api  8940  div11api  8941  sup3exmid  9127  1mhlfehlf  9352  halfpm6th  9354  3halfnz  9567  addex  9876  mulex  9877  unirnioo  10198  nnenom  10686  inftonninf  10694  m1expcl2  10813  i4  10894  expnass  10897  bcn1  11010  hashinfom  11030  abs3difi  11707  0.999...  12072  ef01bndlem  12307  cos1bnd  12310  cos2bnd  12311  sin4lt0  12318  3dvdsdec  12416  3dvds2dec  12417  ndvdsi  12484  flodddiv4  12487  3lcm2e6woprm  12648  6lcm4e12  12649  3prm  12690  dec2dvds  12974  modxai  12979  gcdi  12983  numexp2x  12988  2exp5  12995  2exp11  12999  znnen  13009  ennnfonelem1  13018  prminf  13066  topnfn  13317  prdsvallem  13345  prdsval  13346  fnmgp  13925  rhmex  14161  rmodislmodlem  14354  rmodislmod  14355  cnfldstr  14562  zring0  14604  fnpsr  14671  mplvalcoe  14694  fnmpl  14697  xmetunirn  15072  tgioo  15268  tgqioo  15269  addcncntoplem  15275  expcncf  15323  dveflem  15440  dvef  15441  efcn  15482  sinhalfpilem  15505  sincosq1lem  15539  sincosq4sgn  15543  cosq23lt0  15547  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  pigt3  15558  cos02pilt1  15565  cos0pilt1  15566  2logb9irr  15685  2logb3irr  15687  2logb9irrALT  15688  sqrt2cxp2logb9e3  15689  2irrexpq  15690  2logb9irrap  15691  2irrexpqap  15692  1sgm2ppw  15709  lgseisenlem1  15789  lgseisenlem2  15790  lgsquadlem1  15796  upgr2wlkdc  16172  ex-fl  16257  ex-exp  16259  trilpolemeq1  16580