Theorem mp3an12 1327

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  mp3an12i  1341  ceqsralv  2770  brelrn  4862  funpr  5270  fpm  6683  ener  6781  ltaddnq  7408  ltadd1sr  7777  map2psrprg  7806  mul02  8346  ltapi  8595  div0ap  8661  divclapzi  8706  divcanap1zi  8707  divcanap2zi  8708  divrecapzi  8709  divcanap3zi  8710  divcanap4zi  8711  divassapzi  8721  divmulapzi  8722  divdirapzi  8723  redivclapzi  8737  ltm1  8805  mulgt1  8822  recgt1i  8857  recreclt  8859  ltmul1i  8879  ltdiv1i  8880  ltmuldivi  8881  ltmul2i  8882  lemul1i  8883  lemul2i  8884  cju  8920  nnge1  8944  nngt0  8946  nnrecgt0  8959  elnnnn0c  9223  elnnz1  9278  recnz  9348  eluzsubi  9557  ge0gtmnf  9825  m1expcl2  10544  1exp  10551  m1expeven  10569  expubnd  10579  iexpcyc  10627  expnbnd  10646  expnlbnd  10647  remim  10871  imval2  10905  cjdivapi  10946  absdivapzi  11165  fprodge1  11649  ef01bndlem  11766  sin01gt0  11771  cos01gt0  11772  cos12dec  11777  absefib  11780  efieq1re  11781  zeo3  11875  evend2  11896  cnbl0  14073  reeff1olem  14231  sincosq1sgn  14286  sincosq3sgn  14288  sincosq4sgn  14289  rpelogb  14406  lgsdir2lem2  14469