Theorem mp3an3 1321

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  mp3an13  1323  mp3an23  1324  mp3anl3  1328  opelxp  4639  funimaexg  5280  ov  5969  ovmpoa  5980  ovmpo  5985  ovtposg  6235  oaword1  6447  th3q  6614  enrefg  6738  f1imaen  6768  mapxpen  6822  pw1fin  6884  xpfi  6903  djucomen  7180  addnnnq0  7398  mulnnnq0  7399  prarloclemcalc  7451  genpelxp  7460  genpprecll  7463  genppreclu  7464  addsrpr  7694  mulsrpr  7695  gt0srpr  7697  mulid1  7904  ltneg  8368  leneg  8371  suble0  8382  div1  8607  nnaddcl  8885  nnmulcl  8886  nnge1  8888  nnsub  8904  2halves  9094  halfaddsub  9099  addltmul  9101  zleltp1  9254  nnaddm1cl  9260  zextlt  9291  peano5uzti  9307  eluzp1p1  9499  uzaddcl  9532  znq  9570  xrre  9764  xrre2  9765  fzshftral  10051  expn1ap0  10473  expadd  10505  expmul  10508  expubnd  10520  sqmul  10525  bernneq  10583  sqrecapd  10600  faclbnd2  10663  faclbnd6  10665  fihashssdif  10740  shftval3  10778  caucvgre  10932  leabs  11025  ltabs  11038  caubnd2  11068  efexp  11632  efival  11682  cos01gt0  11712  odd2np1  11819  halfleoddlt  11840  omoe  11842  opeo  11843  gcdmultiple  11962  sqgcd  11971  nn0seqcvgd  11982  phiprmpw  12163  eulerthlemth  12173  odzcllem  12183  pcelnn  12261  4sqlem3  12329  ntrin  12839  txuni2  12971  txopn  12980  xblpnfps  13113  xblpnf  13114  bl2in  13118  unirnblps  13137  unirnbl  13138  blpnfctr  13154  sincosq1eq  13475  rpcxpp1  13542  rplogb1  13581