Theorem mp3an12 1363

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  mp3an12i  1377  ceqsralv  2834  brelrn  4965  funpr  5382  fpm  6850  ener  6953  ltaddnq  7627  ltadd1sr  7996  map2psrprg  8025  mul02  8566  ltapi  8816  div0ap  8882  divclapzi  8927  divcanap1zi  8928  divcanap2zi  8929  divrecapzi  8930  divcanap3zi  8931  divcanap4zi  8932  divassapzi  8942  divmulapzi  8943  divdirapzi  8944  redivclapzi  8958  ltm1  9026  mulgt1  9043  recgt1i  9078  recreclt  9080  ltmul1i  9100  ltdiv1i  9101  ltmuldivi  9102  ltmul2i  9103  lemul1i  9104  lemul2i  9105  cju  9141  nnge1  9166  nngt0  9168  nnrecgt0  9181  elnnnn0c  9447  elnnz1  9502  recnz  9573  eluzsubi  9784  ge0gtmnf  10058  m1expcl2  10824  1exp  10831  m1expeven  10849  expubnd  10859  iexpcyc  10907  expnbnd  10926  expnlbnd  10927  remim  11438  imval2  11472  cjdivapi  11513  absdivapzi  11732  fprodge1  12218  ef01bndlem  12335  sin01gt0  12341  cos01gt0  12342  cos12dec  12347  absefib  12350  efieq1re  12351  zeo3  12447  evend2  12468  cnbl0  15277  reeff1olem  15514  sincosq1sgn  15569  sincosq3sgn  15571  sincosq4sgn  15572  rpelogb  15692  lgsdir2lem2  15777  konigsberglem5  16362