Theorem mp3an12 1309

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

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

Assertion

Ref	Expression
mp3an12	⊢ (𝜒 → 𝜃)

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 ⊢ 𝜓
2		mp3an12.1	. . 3 ⊢ 𝜑
3		mp3an12.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an1 1306	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 421	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 963

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 965

This theorem is referenced by:  mp3an12i  1323  ceqsralv  2743  brelrn  4819  funpr  5222  fpm  6626  ener  6724  ltaddnq  7327  ltadd1sr  7696  map2psrprg  7725  mul02  8262  ltapi  8511  div0ap  8575  divclapzi  8620  divcanap1zi  8621  divcanap2zi  8622  divrecapzi  8623  divcanap3zi  8624  divcanap4zi  8625  divassapzi  8635  divmulapzi  8636  divdirapzi  8637  redivclapzi  8651  ltm1  8717  mulgt1  8734  recgt1i  8769  recreclt  8771  ltmul1i  8791  ltdiv1i  8792  ltmuldivi  8793  ltmul2i  8794  lemul1i  8795  lemul2i  8796  cju  8832  nnge1  8856  nngt0  8858  nnrecgt0  8871  elnnnn0c  9135  elnnz1  9190  recnz  9257  eluzsubi  9466  ge0gtmnf  9727  m1expcl2  10441  1exp  10448  m1expeven  10466  expubnd  10476  iexpcyc  10523  expnbnd  10541  expnlbnd  10542  remim  10760  imval2  10794  cjdivapi  10835  absdivapzi  11054  fprodge1  11536  ef01bndlem  11653  sin01gt0  11658  cos01gt0  11659  cos12dec  11664  absefib  11667  efieq1re  11668  zeo3  11759  evend2  11780  cnbl0  12945  reeff1olem  13103  sincosq1sgn  13158  sincosq3sgn  13160  sincosq4sgn  13161  rpelogb  13277