Theorem mp3an12 1340

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  mp3an12i  1354  ceqsralv  2803  brelrn  4912  funpr  5327  fpm  6770  ener  6873  ltaddnq  7522  ltadd1sr  7891  map2psrprg  7920  mul02  8461  ltapi  8711  div0ap  8777  divclapzi  8822  divcanap1zi  8823  divcanap2zi  8824  divrecapzi  8825  divcanap3zi  8826  divcanap4zi  8827  divassapzi  8837  divmulapzi  8838  divdirapzi  8839  redivclapzi  8853  ltm1  8921  mulgt1  8938  recgt1i  8973  recreclt  8975  ltmul1i  8995  ltdiv1i  8996  ltmuldivi  8997  ltmul2i  8998  lemul1i  8999  lemul2i  9000  cju  9036  nnge1  9061  nngt0  9063  nnrecgt0  9076  elnnnn0c  9342  elnnz1  9397  recnz  9468  eluzsubi  9678  ge0gtmnf  9947  m1expcl2  10708  1exp  10715  m1expeven  10733  expubnd  10743  iexpcyc  10791  expnbnd  10810  expnlbnd  10811  remim  11204  imval2  11238  cjdivapi  11279  absdivapzi  11498  fprodge1  11983  ef01bndlem  12100  sin01gt0  12106  cos01gt0  12107  cos12dec  12112  absefib  12115  efieq1re  12116  zeo3  12212  evend2  12233  cnbl0  15039  reeff1olem  15276  sincosq1sgn  15331  sincosq3sgn  15333  sincosq4sgn  15334  rpelogb  15454  lgsdir2lem2  15539