Theorem mp3an3 1221

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

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  mp3an13  1223  mp3an23  1224  mp3anl3  1228  opelxp  4374  funimaexg  4983  ov  5620  ovmpt2a  5631  ovmpt2  5636  ovtposg  5874  oaword1  6050  th3q  6211  enrefg  6244  f1imaen  6274  addnnnq0  6547  mulnnnq0  6548  prarloclemcalc  6600  genpelxp  6609  genpprecll  6612  genppreclu  6613  addsrpr  6830  mulsrpr  6831  gt0srpr  6833  mulid1  7024  ltneg  7457  leneg  7460  suble0  7471  div1  7680  nnaddcl  7934  nnmulcl  7935  nnge1  7937  nnsub  7952  2halves  8154  halfaddsub  8159  addltmul  8161  zleltp1  8299  nnaddm1cl  8305  zextlt  8332  peano5uzti  8346  eluzp1p1  8498  uzaddcl  8529  znq  8559  xrre  8733  xrre2  8734  fzshftral  8970  expn1ap0  9265  expadd  9297  expmul  9300  expubnd  9311  sqmul  9316  bernneq  9369  sqrecapd  9385  shftval3  9428  caucvgre  9580  leabs  9672  ltabs  9683  caubnd2  9713  nn0seqcvgd  9880