Theorem mp3an12 1270

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

Syntax hints:   → wi 4   ∧ w3a 927

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

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

This theorem is referenced by:  mp3an12i  1284  ceqsralv  2664  brelrn  4700  funpr  5100  fpm  6478  ener  6576  ltaddnq  7063  ltadd1sr  7419  mul02  7962  ltapi  8208  div0ap  8266  divclapzi  8311  divcanap1zi  8312  divcanap2zi  8313  divrecapzi  8314  divcanap3zi  8315  divcanap4zi  8316  divassapzi  8326  divmulapzi  8327  divdirapzi  8328  redivclapzi  8342  ltm1  8404  mulgt1  8421  recgt1i  8456  recreclt  8458  ltmul1i  8478  ltdiv1i  8479  ltmuldivi  8480  ltmul2i  8481  lemul1i  8482  lemul2i  8483  cju  8519  nnge1  8543  nngt0  8545  nnrecgt0  8558  elnnnn0c  8816  elnnz1  8871  recnz  8938  eluzsubi  9145  ge0gtmnf  9389  m1expcl2  10092  1exp  10099  m1expeven  10117  expubnd  10127  iexpcyc  10174  expnbnd  10192  expnlbnd  10193  remim  10409  imval2  10443  cjdivapi  10484  absdivapzi  10702  ef01bndlem  11196  sin01gt0  11201  cos01gt0  11202  absefib  11209  efieq1re  11210  zeo3  11295  evend2  11316  cnbl0  12311