Theorem mp3an 1271

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

Syntax hints:   → wi 4   ∧ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  vtocl3  2669  raltp  3481  rextp  3482  ordtriexmidlem  4307  ordtri2or2exmidlem  4313  onsucelsucexmidlem  4316  ordsoexmid  4349  funopg  5009  ftp  5438  caovass  5755  caovdi  5774  ofmres  5857  mpt2fvexi  5926  dmtpos  5968  rntpos  5969  dftpos3  5974  tpostpos  5976  mapsnen  6473  xpcomen  6488  mapxpen  6509  xpmapenlem  6510  unfiexmid  6573  1lt2pi  6835  1lt2nq  6901  halfnqq  6905  m1p1sr  7242  m1m1sr  7243  addassi  7432  mulassi  7433  adddii  7434  adddiri  7435  lttri  7525  lelttri  7526  ltletri  7527  letri  7528  mul12i  7564  mul32i  7565  add12i  7581  add32i  7582  addcani  7600  addcan2i  7601  subaddi  7705  subadd2i  7706  subsub23i  7708  addsubassi  7709  addsubi  7710  subcani  7711  subcan2i  7712  pnncani  7713  subdii  7821  subdiri  7822  ltadd2i  7834  ltadd1i  7913  leadd1i  7914  leadd2i  7915  ltsubaddi  7916  lesubaddi  7917  ltsubadd2i  7918  lesubadd2i  7919  ltaddsubi  7920  gtapii  8042  mulcanapi  8067  divclapi  8152  divcanap2i  8153  divcanap1i  8154  divrecapi  8155  divcanap3i  8156  divcanap4i  8157  divassapi  8166  divdirapi  8167  div23api  8168  div11api  8169  1mhlfehlf  8559  halfpm6th  8561  3halfnz  8768  unirnioo  9315  nnenom  9761  inftonninf  9767  m1expcl2  9867  i4  9946  expnass  9949  bcn1  10054  hashinfom  10074  abs3difi  10476  3dvdsdec  10731  3dvds2dec  10732  ndvdsi  10799  flodddiv4  10800  3lcm2e6woprm  10934  6lcm4e12  10935  3prm  10976  znnen  11077  ex-fl  11082