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  8715  ltapi  8966  div0ap  9034  divclapzi  9079  divcanap1zi  9080  divcanap2zi  9081  divrecapzi  9082  divcanap3zi  9083  divcanap4zi  9084  divassapzi  9094  divmulapzi  9095  divdirapzi  9096  redivclapzi  9110  ltm1  9178  mulgt1  9195  recgt1i  9230  recreclt  9232  ltmul1i  9252  ltdiv1i  9253  ltmuldivi  9254  ltmul2i  9255  lemul1i  9256  lemul2i  9257  cju  9293  nnge1  9329  nngt0  9331  nnrecgt0  9344  elnnnn0c  9612  elnnz1  9671  recnz  9743  eluzsubi  9959  ge0gtmnf  10235  m1expcl2  11011  1exp  11018  m1expeven  11036  expubnd  11046  iexpcyc  11094  resq01  11108  expnbnd  11114  expnlbnd  11115  remim  11639  imval2  11673  cjdivapi  11715  absdivapzi  11935  fprodge1  12422  ef01bndlem  12539  sin01gt0  12545  cos01gt0  12546  cos12dec  12551  absefib  12554  efieq1re  12555  zeo3  12651  evend2  12672  prmlem1  13242  prmlem2  13254  cnbl0  15684  reeff1olem  15921  sincosq1sgn  15977  sincosq3sgn  15979  sincosq4sgn  15980  rpelogb  16104  lgsdir2lem2  16246  konigsberglem5  16831