Theorem mp3an3 1367

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 1236	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 15	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

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

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 1011

This theorem is referenced by:  mp3an13  1369  mp3an23  1370  mp3anl3  1374  opelxp  4799  funimaexg  5460  ov  6198  ovmpoa  6209  ovmpo  6214  ovtposg  6520  oaword1  6734  th3q  6904  enrefg  7040  f1imaen  7071  mapxpen  7138  pw1fin  7207  xpfi  7229  djucomen  7562  addnnnq0  7806  mulnnnq0  7807  prarloclemcalc  7859  genpelxp  7868  genpprecll  7871  genppreclu  7872  addsrpr  8102  mulsrpr  8103  gt0srpr  8105  mulrid  8313  ltneg  8780  leneg  8783  suble0  8794  div1  9023  nnaddcl  9303  nnmulcl  9304  nnge1  9306  nnsub  9322  2halves  9513  halfaddsub  9518  addltmul  9521  fcdmnn0fsuppg  9597  zleltp1  9679  nnaddm1cl  9685  zextlt  9717  peano5uzti  9733  eluzp1p1  9927  uzaddcl  9965  znq  10003  xrre  10201  xrre2  10202  fzshftral  10493  nninfinf  10858  expn1ap0  10964  expadd  10996  expmul  10999  expubnd  11011  sqmul  11016  bernneq  11076  sqrecapd  11093  faclbnd2  11158  faclbnd6  11160  fihashssdif  11237  ccatlcan  11468  ccatrcan  11469  shftval3  11570  caucvgre  11725  leabs  11818  ltabs  11831  caubnd2  11861  efexp  12427  efival  12477  cos01gt0  12508  odd2np1  12618  halfleoddlt  12639  omoe  12641  opeo  12642  gcdmultiple  12775  sqgcd  12784  nn0seqcvgd  12797  phiprmpw  12978  eulerthlemth  12988  odzcllem  12999  pcelnn  13078  4sqlem3  13147  lsp0  14732  lss0v  14739  zndvds0  14957  ntrin  15148  txuni2  15280  txopn  15289  xblpnfps  15422  xblpnf  15423  bl2in  15427  unirnblps  15446  unirnbl  15447  blpnfctr  15463  plyconst  15769  plyid  15770  sincosq1eq  15863  rpcxpp1  15931  rplogb1  15973