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  6849  ener  6952  ltaddnq  7626  ltadd1sr  7995  map2psrprg  8024  mul02  8565  ltapi  8815  div0ap  8881  divclapzi  8926  divcanap1zi  8927  divcanap2zi  8928  divrecapzi  8929  divcanap3zi  8930  divcanap4zi  8931  divassapzi  8941  divmulapzi  8942  divdirapzi  8943  redivclapzi  8957  ltm1  9025  mulgt1  9042  recgt1i  9077  recreclt  9079  ltmul1i  9099  ltdiv1i  9100  ltmuldivi  9101  ltmul2i  9102  lemul1i  9103  lemul2i  9104  cju  9140  nnge1  9165  nngt0  9167  nnrecgt0  9180  elnnnn0c  9446  elnnz1  9501  recnz  9572  eluzsubi  9783  ge0gtmnf  10057  m1expcl2  10822  1exp  10829  m1expeven  10847  expubnd  10857  iexpcyc  10905  expnbnd  10924  expnlbnd  10925  remim  11420  imval2  11454  cjdivapi  11495  absdivapzi  11714  fprodge1  12199  ef01bndlem  12316  sin01gt0  12322  cos01gt0  12323  cos12dec  12328  absefib  12331  efieq1re  12332  zeo3  12428  evend2  12449  cnbl0  15257  reeff1olem  15494  sincosq1sgn  15549  sincosq3sgn  15551  sincosq4sgn  15552  rpelogb  15672  lgsdir2lem2  15757