Theorem mp3an3 1304

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

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

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 964

This theorem is referenced by:  mp3an13  1306  mp3an23  1307  mp3anl3  1311  opelxp  4569  funimaexg  5207  ov  5890  ovmpoa  5901  ovmpo  5906  ovtposg  6156  oaword1  6367  th3q  6534  enrefg  6658  f1imaen  6688  mapxpen  6742  xpfi  6818  djucomen  7072  addnnnq0  7257  mulnnnq0  7258  prarloclemcalc  7310  genpelxp  7319  genpprecll  7322  genppreclu  7323  addsrpr  7553  mulsrpr  7554  gt0srpr  7556  mulid1  7763  ltneg  8224  leneg  8227  suble0  8238  div1  8463  nnaddcl  8740  nnmulcl  8741  nnge1  8743  nnsub  8759  2halves  8949  halfaddsub  8954  addltmul  8956  zleltp1  9109  nnaddm1cl  9115  zextlt  9143  peano5uzti  9159  eluzp1p1  9351  uzaddcl  9381  znq  9416  xrre  9603  xrre2  9604  fzshftral  9888  expn1ap0  10303  expadd  10335  expmul  10338  expubnd  10350  sqmul  10355  bernneq  10412  sqrecapd  10428  faclbnd2  10488  faclbnd6  10490  fihashssdif  10564  shftval3  10599  caucvgre  10753  leabs  10846  ltabs  10859  caubnd2  10889  efexp  11388  efival  11439  cos01gt0  11469  odd2np1  11570  halfleoddlt  11591  omoe  11593  opeo  11594  gcdmultiple  11708  sqgcd  11717  nn0seqcvgd  11722  phiprmpw  11898  ntrin  12293  txuni2  12425  txopn  12434  xblpnfps  12567  xblpnf  12568  bl2in  12572  unirnblps  12591  unirnbl  12592  blpnfctr  12608  sincosq1eq  12920