Theorem mp3an3 1287

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

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

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

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

This theorem is referenced by:  mp3an13  1289  mp3an23  1290  mp3anl3  1294  opelxp  4529  funimaexg  5165  ov  5844  ovmpoa  5855  ovmpo  5860  ovtposg  6110  oaword1  6321  th3q  6488  enrefg  6612  f1imaen  6642  mapxpen  6695  xpfi  6771  djucomen  7020  addnnnq0  7205  mulnnnq0  7206  prarloclemcalc  7258  genpelxp  7267  genpprecll  7270  genppreclu  7271  addsrpr  7488  mulsrpr  7489  gt0srpr  7491  mulid1  7687  ltneg  8143  leneg  8146  suble0  8157  div1  8376  nnaddcl  8650  nnmulcl  8651  nnge1  8653  nnsub  8669  2halves  8853  halfaddsub  8858  addltmul  8860  zleltp1  9013  nnaddm1cl  9019  zextlt  9047  peano5uzti  9063  eluzp1p1  9253  uzaddcl  9283  znq  9318  xrre  9496  xrre2  9497  fzshftral  9781  expn1ap0  10196  expadd  10228  expmul  10231  expubnd  10243  sqmul  10248  bernneq  10305  sqrecapd  10321  faclbnd2  10381  faclbnd6  10383  fihashssdif  10457  shftval3  10492  caucvgre  10645  leabs  10738  ltabs  10751  caubnd2  10781  efexp  11239  efival  11290  cos01gt0  11320  odd2np1  11418  halfleoddlt  11439  omoe  11441  opeo  11442  gcdmultiple  11554  sqgcd  11563  nn0seqcvgd  11568  phiprmpw  11743  ntrin  12136  txuni2  12267  txopn  12276  xblpnfps  12387  xblpnf  12388  bl2in  12392  unirnblps  12411  unirnbl  12412  blpnfctr  12428