Theorem mp3an12 1368

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3an12i  1382  ceqsralv  2853  brelrn  5015  funpr  5433  fpm  6962  ener  7066  0fsupp  7298  ltaddnq  7774  ltadd1sr  8143  map2psrprg  8172  mul02  8714  ltapi  8964  div0ap  9032  divclapzi  9077  divcanap1zi  9078  divcanap2zi  9079  divrecapzi  9080  divcanap3zi  9081  divcanap4zi  9082  divassapzi  9092  divmulapzi  9093  divdirapzi  9094  redivclapzi  9108  ltm1  9176  mulgt1  9193  recgt1i  9228  recreclt  9230  ltmul1i  9250  ltdiv1i  9251  ltmuldivi  9252  ltmul2i  9253  lemul1i  9254  lemul2i  9255  cju  9291  nnge1  9327  nngt0  9329  nnrecgt0  9342  elnnnn0c  9608  elnnz1  9667  recnz  9739  eluzsubi  9950  ge0gtmnf  10225  m1expcl2  10998  1exp  11005  m1expeven  11023  expubnd  11033  iexpcyc  11081  resq01  11095  expnbnd  11101  expnlbnd  11102  remim  11625  imval2  11659  cjdivapi  11701  absdivapzi  11920  fprodge1  12406  ef01bndlem  12523  sin01gt0  12529  cos01gt0  12530  cos12dec  12535  absefib  12538  efieq1re  12539  zeo3  12635  evend2  12656  cnbl0  15635  reeff1olem  15872  sincosq1sgn  15927  sincosq3sgn  15929  sincosq4sgn  15930  rpelogb  16051  lgsdir2lem2  16148  konigsberglem5  16733