Theorem mp3an3 1337

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

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

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 982

This theorem is referenced by:  mp3an13  1339  mp3an23  1340  mp3anl3  1344  opelxp  4694  funimaexg  5343  ov  6046  ovmpoa  6057  ovmpo  6062  ovtposg  6326  oaword1  6538  th3q  6708  enrefg  6832  f1imaen  6862  mapxpen  6918  pw1fin  6980  xpfi  7002  djucomen  7301  addnnnq0  7535  mulnnnq0  7536  prarloclemcalc  7588  genpelxp  7597  genpprecll  7600  genppreclu  7601  addsrpr  7831  mulsrpr  7832  gt0srpr  7834  mulrid  8042  ltneg  8508  leneg  8511  suble0  8522  div1  8749  nnaddcl  9029  nnmulcl  9030  nnge1  9032  nnsub  9048  2halves  9239  halfaddsub  9244  addltmul  9247  zleltp1  9400  nnaddm1cl  9406  zextlt  9437  peano5uzti  9453  eluzp1p1  9646  uzaddcl  9679  znq  9717  xrre  9914  xrre2  9915  fzshftral  10202  nninfinf  10554  expn1ap0  10660  expadd  10692  expmul  10695  expubnd  10707  sqmul  10712  bernneq  10771  sqrecapd  10788  faclbnd2  10853  faclbnd6  10855  fihashssdif  10929  shftval3  11011  caucvgre  11165  leabs  11258  ltabs  11271  caubnd2  11301  efexp  11866  efival  11916  cos01gt0  11947  odd2np1  12057  halfleoddlt  12078  omoe  12080  opeo  12081  gcdmultiple  12214  sqgcd  12223  nn0seqcvgd  12236  phiprmpw  12417  eulerthlemth  12427  odzcllem  12438  pcelnn  12517  4sqlem3  12586  lsp0  14057  lss0v  14064  zndvds0  14284  ntrin  14468  txuni2  14600  txopn  14609  xblpnfps  14742  xblpnf  14743  bl2in  14747  unirnblps  14766  unirnbl  14767  blpnfctr  14783  plyconst  15089  plyid  15090  sincosq1eq  15183  rpcxpp1  15250  rplogb1  15292