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  6733  oeiv  6734  omv2  6743  1idprl  7963  muladd11  8466  negsub  8581  subneg  8582  ltaddneg  8759  muleqadd  9006  diveqap1  9043  conjmulap  9067  nnsub  9352  addltmul  9553  zltp1le  9708  gtndiv  9751  eluzp1m1  9961  xnn0le2is012  10284  divelunit  10420  fznatpl1  10499  flqbi2  10746  flqdiv  10778  frecfzen2  10884  nn0ennn  10890  seqshft2g  10939  seqf1oglem1  10976  faclbnd3  11202  ccatrid  11396  shftfvalg  11604  ovshftex  11605  shftfval  11607  abs2dif  11894  cos2t  12541  sin01gt0  12553  cos01gt0  12554  demoivre  12564  demoivreALT  12565  omeo  12689  gcd0id  12780  sqgcd  12830  isprm3  12920  eulerthlemth  13038  pczpre  13104  pcrec  13115  setscom  13449  setsslid  13460  setsslnid  13461  mulgm1  14003  abssinper  16090  ppiqub  16310  chtqub  16313  bposlem2  16329  lgs1  16385