Theorem mp3an3 1360

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

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

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 1004

This theorem is referenced by:  mp3an13  1362  mp3an23  1363  mp3anl3  1367  opelxp  4749  funimaexg  5405  ov  6124  ovmpoa  6135  ovmpo  6140  ovtposg  6405  oaword1  6617  th3q  6787  enrefg  6915  f1imaen  6946  mapxpen  7009  pw1fin  7072  xpfi  7094  djucomen  7398  addnnnq0  7636  mulnnnq0  7637  prarloclemcalc  7689  genpelxp  7698  genpprecll  7701  genppreclu  7702  addsrpr  7932  mulsrpr  7933  gt0srpr  7935  mulrid  8143  ltneg  8609  leneg  8612  suble0  8623  div1  8850  nnaddcl  9130  nnmulcl  9131  nnge1  9133  nnsub  9149  2halves  9340  halfaddsub  9345  addltmul  9348  zleltp1  9502  nnaddm1cl  9508  zextlt  9539  peano5uzti  9555  eluzp1p1  9748  uzaddcl  9781  znq  9819  xrre  10016  xrre2  10017  fzshftral  10304  nninfinf  10665  expn1ap0  10771  expadd  10803  expmul  10806  expubnd  10818  sqmul  10823  bernneq  10882  sqrecapd  10899  faclbnd2  10964  faclbnd6  10966  fihashssdif  11040  ccatlcan  11250  ccatrcan  11251  shftval3  11338  caucvgre  11492  leabs  11585  ltabs  11598  caubnd2  11628  efexp  12193  efival  12243  cos01gt0  12274  odd2np1  12384  halfleoddlt  12405  omoe  12407  opeo  12408  gcdmultiple  12541  sqgcd  12550  nn0seqcvgd  12563  phiprmpw  12744  eulerthlemth  12754  odzcllem  12765  pcelnn  12844  4sqlem3  12913  lsp0  14387  lss0v  14394  zndvds0  14614  ntrin  14798  txuni2  14930  txopn  14939  xblpnfps  15072  xblpnf  15073  bl2in  15077  unirnblps  15096  unirnbl  15097  blpnfctr  15113  plyconst  15419  plyid  15420  sincosq1eq  15513  rpcxpp1  15580  rplogb1  15622