Theorem mp3an12 1364

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  mp3an12i  1378  ceqsralv  2835  brelrn  4971  funpr  5389  fpm  6893  ener  6996  ltaddnq  7670  ltadd1sr  8039  map2psrprg  8068  mul02  8609  ltapi  8859  div0ap  8925  divclapzi  8970  divcanap1zi  8971  divcanap2zi  8972  divrecapzi  8973  divcanap3zi  8974  divcanap4zi  8975  divassapzi  8985  divmulapzi  8986  divdirapzi  8987  redivclapzi  9001  ltm1  9069  mulgt1  9086  recgt1i  9121  recreclt  9123  ltmul1i  9143  ltdiv1i  9144  ltmuldivi  9145  ltmul2i  9146  lemul1i  9147  lemul2i  9148  cju  9184  nnge1  9209  nngt0  9211  nnrecgt0  9224  elnnnn0c  9490  elnnz1  9545  recnz  9616  eluzsubi  9827  ge0gtmnf  10101  m1expcl2  10867  1exp  10874  m1expeven  10892  expubnd  10902  iexpcyc  10950  expnbnd  10969  expnlbnd  10970  remim  11481  imval2  11515  cjdivapi  11556  absdivapzi  11775  fprodge1  12261  ef01bndlem  12378  sin01gt0  12384  cos01gt0  12385  cos12dec  12390  absefib  12393  efieq1re  12394  zeo3  12490  evend2  12511  cnbl0  15325  reeff1olem  15562  sincosq1sgn  15617  sincosq3sgn  15619  sincosq4sgn  15620  rpelogb  15740  lgsdir2lem2  15828  konigsberglem5  16413