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  4532  ordsuc  4712  omv  6732  oeiv  6733  omv2  6742  1idprl  7963  muladd11  8466  negsub  8581  subneg  8582  ltaddneg  8759  muleqadd  9006  diveqap1  9043  conjmulap  9067  nnsub  9352  addltmul  9553  zltp1le  9710  gtndiv  9752  eluzp1m1  9962  xnn0le2is012  10285  divelunit  10421  fznatpl1  10500  flqbi2  10747  flqdiv  10779  frecfzen2  10885  nn0ennn  10891  seqshft2g  10940  seqf1oglem1  10977  faclbnd3  11203  ccatrid  11397  shftfvalg  11605  ovshftex  11606  shftfval  11608  abs2dif  11895  cos2t  12542  sin01gt0  12554  cos01gt0  12555  demoivre  12565  demoivreALT  12566  omeo  12690  gcd0id  12781  sqgcd  12831  isprm3  12921  eulerthlemth  13039  pczpre  13105  pcrec  13116  setscom  13450  setsslid  13461  setsslnid  13462  mulgm1  14004  abssinper  16073  ppiqub  16293  chtqub  16296  bposlem2  16312  lgs1  16368