Theorem mp3an3 1260

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 922

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

This theorem depends on definitions:  df-bi 115  df-3an 924

This theorem is referenced by:  mp3an13  1262  mp3an23  1263  mp3anl3  1267  opelxp  4440  funimaexg  5063  ov  5721  ovmpt2a  5732  ovmpt2  5737  ovtposg  5978  oaword1  6186  th3q  6349  enrefg  6433  f1imaen  6463  mapxpen  6516  xpfi  6590  addnnnq0  6952  mulnnnq0  6953  prarloclemcalc  7005  genpelxp  7014  genpprecll  7017  genppreclu  7018  addsrpr  7235  mulsrpr  7236  gt0srpr  7238  mulid1  7429  ltneg  7884  leneg  7887  suble0  7898  div1  8109  nnaddcl  8377  nnmulcl  8378  nnge1  8380  nnsub  8395  2halves  8578  halfaddsub  8583  addltmul  8585  zleltp1  8738  nnaddm1cl  8744  zextlt  8771  peano5uzti  8787  eluzp1p1  8976  uzaddcl  9006  znq  9041  xrre  9214  xrre2  9215  fzshftral  9452  expn1ap0  9863  expadd  9895  expmul  9898  expubnd  9910  sqmul  9915  bernneq  9970  sqrecapd  9986  faclbnd2  10046  faclbnd6  10048  fihashssdif  10122  shftval3  10157  caucvgre  10309  leabs  10402  ltabs  10415  caubnd2  10445  odd2np1  10748  halfleoddlt  10769  omoe  10771  opeo  10772  gcdmultiple  10884  sqgcd  10893  nn0seqcvgd  10898  phiprmpw  11073