Theorem mp3an2 1366

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	⊢ 𝜓
mp3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1234	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 439	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  mp3anl2  1373  ordin  4530  ordsuc  4710  omv  6728  oeiv  6729  omv2  6738  1idprl  7957  muladd11  8460  negsub  8575  subneg  8576  ltaddneg  8753  muleqadd  9000  diveqap1  9037  conjmulap  9061  nnsub  9345  addltmul  9546  zltp1le  9703  gtndiv  9745  eluzp1m1  9955  xnn0le2is012  10278  divelunit  10414  fznatpl1  10493  flqbi2  10739  flqdiv  10771  frecfzen2  10877  nn0ennn  10883  seqshft2g  10932  seqf1oglem1  10969  faclbnd3  11195  ccatrid  11389  shftfvalg  11597  ovshftex  11598  shftfval  11600  abs2dif  11887  cos2t  12533  sin01gt0  12545  cos01gt0  12546  demoivre  12556  demoivreALT  12557  omeo  12681  gcd0id  12772  sqgcd  12822  isprm3  12912  eulerthlemth  13030  pczpre  13096  pcrec  13107  setscom  13441  setsslid  13452  setsslnid  13453  mulgm1  13994  abssinper  15997  ppiqub  16194  bposlem2  16210  lgs1  16261