Theorem mp3an3 1339

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

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

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 983

This theorem is referenced by:  mp3an13  1341  mp3an23  1342  mp3anl3  1346  opelxp  4706  funimaexg  5359  ov  6067  ovmpoa  6078  ovmpo  6083  ovtposg  6347  oaword1  6559  th3q  6729  enrefg  6857  f1imaen  6888  mapxpen  6947  pw1fin  7009  xpfi  7031  djucomen  7330  addnnnq0  7564  mulnnnq0  7565  prarloclemcalc  7617  genpelxp  7626  genpprecll  7629  genppreclu  7630  addsrpr  7860  mulsrpr  7861  gt0srpr  7863  mulrid  8071  ltneg  8537  leneg  8540  suble0  8551  div1  8778  nnaddcl  9058  nnmulcl  9059  nnge1  9061  nnsub  9077  2halves  9268  halfaddsub  9273  addltmul  9276  zleltp1  9430  nnaddm1cl  9436  zextlt  9467  peano5uzti  9483  eluzp1p1  9676  uzaddcl  9709  znq  9747  xrre  9944  xrre2  9945  fzshftral  10232  nninfinf  10590  expn1ap0  10696  expadd  10728  expmul  10731  expubnd  10743  sqmul  10748  bernneq  10807  sqrecapd  10824  faclbnd2  10889  faclbnd6  10891  fihashssdif  10965  shftval3  11171  caucvgre  11325  leabs  11418  ltabs  11431  caubnd2  11461  efexp  12026  efival  12076  cos01gt0  12107  odd2np1  12217  halfleoddlt  12238  omoe  12240  opeo  12241  gcdmultiple  12374  sqgcd  12383  nn0seqcvgd  12396  phiprmpw  12577  eulerthlemth  12587  odzcllem  12598  pcelnn  12677  4sqlem3  12746  lsp0  14218  lss0v  14225  zndvds0  14445  ntrin  14629  txuni2  14761  txopn  14770  xblpnfps  14903  xblpnf  14904  bl2in  14908  unirnblps  14927  unirnbl  14928  blpnfctr  14944  plyconst  15250  plyid  15251  sincosq1eq  15344  rpcxpp1  15411  rplogb1  15453