Theorem mp3an3 1326

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1205	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 15	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

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 980

This theorem is referenced by:  mp3an13  1328  mp3an23  1329  mp3anl3  1333  opelxp  4658  funimaexg  5302  ov  5996  ovmpoa  6007  ovmpo  6012  ovtposg  6262  oaword1  6474  th3q  6642  enrefg  6766  f1imaen  6796  mapxpen  6850  pw1fin  6912  xpfi  6931  djucomen  7217  addnnnq0  7450  mulnnnq0  7451  prarloclemcalc  7503  genpelxp  7512  genpprecll  7515  genppreclu  7516  addsrpr  7746  mulsrpr  7747  gt0srpr  7749  mulrid  7956  ltneg  8421  leneg  8424  suble0  8435  div1  8662  nnaddcl  8941  nnmulcl  8942  nnge1  8944  nnsub  8960  2halves  9150  halfaddsub  9155  addltmul  9157  zleltp1  9310  nnaddm1cl  9316  zextlt  9347  peano5uzti  9363  eluzp1p1  9555  uzaddcl  9588  znq  9626  xrre  9822  xrre2  9823  fzshftral  10110  expn1ap0  10532  expadd  10564  expmul  10567  expubnd  10579  sqmul  10584  bernneq  10643  sqrecapd  10660  faclbnd2  10724  faclbnd6  10726  fihashssdif  10800  shftval3  10838  caucvgre  10992  leabs  11085  ltabs  11098  caubnd2  11128  efexp  11692  efival  11742  cos01gt0  11772  odd2np1  11880  halfleoddlt  11901  omoe  11903  opeo  11904  gcdmultiple  12023  sqgcd  12032  nn0seqcvgd  12043  phiprmpw  12224  eulerthlemth  12234  odzcllem  12244  pcelnn  12322  4sqlem3  12390  ntrin  13663  txuni2  13795  txopn  13804  xblpnfps  13937  xblpnf  13938  bl2in  13942  unirnblps  13961  unirnbl  13962  blpnfctr  13978  sincosq1eq  14299  rpcxpp1  14366  rplogb1  14405