Theorem mp3an12 1305

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

Syntax hints:   → wi 4   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  mp3an12i  1319  ceqsralv  2712  brelrn  4767  funpr  5170  fpm  6568  ener  6666  ltaddnq  7208  ltadd1sr  7577  map2psrprg  7606  mul02  8142  ltapi  8391  div0ap  8455  divclapzi  8500  divcanap1zi  8501  divcanap2zi  8502  divrecapzi  8503  divcanap3zi  8504  divcanap4zi  8505  divassapzi  8515  divmulapzi  8516  divdirapzi  8517  redivclapzi  8531  ltm1  8597  mulgt1  8614  recgt1i  8649  recreclt  8651  ltmul1i  8671  ltdiv1i  8672  ltmuldivi  8673  ltmul2i  8674  lemul1i  8675  lemul2i  8676  cju  8712  nnge1  8736  nngt0  8738  nnrecgt0  8751  elnnnn0c  9015  elnnz1  9070  recnz  9137  eluzsubi  9346  ge0gtmnf  9599  m1expcl2  10308  1exp  10315  m1expeven  10333  expubnd  10343  iexpcyc  10390  expnbnd  10408  expnlbnd  10409  remim  10625  imval2  10659  cjdivapi  10700  absdivapzi  10919  ef01bndlem  11452  sin01gt0  11457  cos01gt0  11458  cos12dec  11463  absefib  11466  efieq1re  11467  zeo3  11554  evend2  11575  cnbl0  12692  sincosq1sgn  12896  sincosq3sgn  12898  sincosq4sgn  12899