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  4564  funimaexg  5202  ov  5883  ovmpoa  5894  ovmpo  5899  ovtposg  6149  oaword1  6360  th3q  6527  enrefg  6651  f1imaen  6681  mapxpen  6735  xpfi  6811  djucomen  7065  addnnnq0  7250  mulnnnq0  7251  prarloclemcalc  7303  genpelxp  7312  genpprecll  7315  genppreclu  7316  addsrpr  7546  mulsrpr  7547  gt0srpr  7549  mulid1  7756  ltneg  8217  leneg  8220  suble0  8231  div1  8456  nnaddcl  8733  nnmulcl  8734  nnge1  8736  nnsub  8752  2halves  8942  halfaddsub  8947  addltmul  8949  zleltp1  9102  nnaddm1cl  9108  zextlt  9136  peano5uzti  9152  eluzp1p1  9344  uzaddcl  9374  znq  9409  xrre  9596  xrre2  9597  fzshftral  9881  expn1ap0  10296  expadd  10328  expmul  10331  expubnd  10343  sqmul  10348  bernneq  10405  sqrecapd  10421  faclbnd2  10481  faclbnd6  10483  fihashssdif  10557  shftval3  10592  caucvgre  10746  leabs  10839  ltabs  10852  caubnd2  10882  efexp  11377  efival  11428  cos01gt0  11458  odd2np1  11559  halfleoddlt  11580  omoe  11582  opeo  11583  gcdmultiple  11697  sqgcd  11706  nn0seqcvgd  11711  phiprmpw  11887  ntrin  12282  txuni2  12414  txopn  12423  xblpnfps  12556  xblpnf  12557  bl2in  12561  unirnblps  12580  unirnbl  12581  blpnfctr  12597  sincosq1eq  12909