Theorem mp3an12 1337

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 1334	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 424	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 979

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 981

This theorem is referenced by:  mp3an12i  1351  ceqsralv  2782  brelrn  4874  funpr  5282  fpm  6698  ener  6796  ltaddnq  7423  ltadd1sr  7792  map2psrprg  7821  mul02  8361  ltapi  8610  div0ap  8676  divclapzi  8721  divcanap1zi  8722  divcanap2zi  8723  divrecapzi  8724  divcanap3zi  8725  divcanap4zi  8726  divassapzi  8736  divmulapzi  8737  divdirapzi  8738  redivclapzi  8752  ltm1  8820  mulgt1  8837  recgt1i  8872  recreclt  8874  ltmul1i  8894  ltdiv1i  8895  ltmuldivi  8896  ltmul2i  8897  lemul1i  8898  lemul2i  8899  cju  8935  nnge1  8959  nngt0  8961  nnrecgt0  8974  elnnnn0c  9238  elnnz1  9293  recnz  9363  eluzsubi  9572  ge0gtmnf  9840  m1expcl2  10559  1exp  10566  m1expeven  10584  expubnd  10594  iexpcyc  10642  expnbnd  10661  expnlbnd  10662  remim  10886  imval2  10920  cjdivapi  10961  absdivapzi  11180  fprodge1  11664  ef01bndlem  11781  sin01gt0  11786  cos01gt0  11787  cos12dec  11792  absefib  11795  efieq1re  11796  zeo3  11890  evend2  11911  cnbl0  14417  reeff1olem  14575  sincosq1sgn  14630  sincosq3sgn  14632  sincosq4sgn  14633  rpelogb  14750  lgsdir2lem2  14813