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  4674  funimaexg  5319  ov  6017  ovmpoa  6028  ovmpo  6033  ovtposg  6285  oaword1  6497  th3q  6667  enrefg  6791  f1imaen  6821  mapxpen  6877  pw1fin  6939  xpfi  6959  djucomen  7246  addnnnq0  7479  mulnnnq0  7480  prarloclemcalc  7532  genpelxp  7541  genpprecll  7544  genppreclu  7545  addsrpr  7775  mulsrpr  7776  gt0srpr  7778  mulrid  7985  ltneg  8450  leneg  8453  suble0  8464  div1  8691  nnaddcl  8970  nnmulcl  8971  nnge1  8973  nnsub  8989  2halves  9179  halfaddsub  9184  addltmul  9186  zleltp1  9339  nnaddm1cl  9345  zextlt  9376  peano5uzti  9392  eluzp1p1  9585  uzaddcl  9618  znq  9656  xrre  9852  xrre2  9853  fzshftral  10140  expn1ap0  10564  expadd  10596  expmul  10599  expubnd  10611  sqmul  10616  bernneq  10675  sqrecapd  10692  faclbnd2  10757  faclbnd6  10759  fihashssdif  10833  shftval3  10871  caucvgre  11025  leabs  11118  ltabs  11131  caubnd2  11161  efexp  11725  efival  11775  cos01gt0  11805  odd2np1  11913  halfleoddlt  11934  omoe  11936  opeo  11937  gcdmultiple  12056  sqgcd  12065  nn0seqcvgd  12076  phiprmpw  12257  eulerthlemth  12267  odzcllem  12277  pcelnn  12356  4sqlem3  12425  lsp0  13756  lss0v  13763  ntrin  14101  txuni2  14233  txopn  14242  xblpnfps  14375  xblpnf  14376  bl2in  14380  unirnblps  14399  unirnbl  14400  blpnfctr  14416  sincosq1eq  14737  rpcxpp1  14804  rplogb1  14843