Theorem syld3an3 1411

Description: A syllogism inference. (Contributed by NM, 20-May-2007.)

Hypotheses

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

Assertion

Ref	Expression
syld3an3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  brelrng  5876  resin  6780  moriotass  7330  omwordri  8482  oewordri  8502  dif1en  9066  sdomdomtrfi  9105  php3  9113  onomeneq  9118  preleqg  9500  gchaleph2  10558  gruf  10697  nnncan1  11392  lediv1  11982  lemuldiv  11997  suprfinzcl  12582  supxrbnd  13222  bcval4  14209  ccatval3  14481  ccatfv0  14486  ccatval1lsw  14487  ccatval21sw  14488  lswccatn0lsw  14494  pfxsuff1eqwrdeq  14601  pfxccatid  14643  cshwidxmodr  14706  2swrd2eqwrdeq  14855  dvdsmultr1  16202  dvdssub2  16207  ndvdsadd  16316  mrcsscl  17521  latnle  18374  latabs1  18376  latabs2  18377  latj4rot  18391  grpsubf  18927  grpinvsub  18930  grpnpcan  18940  mulginvcom  19007  mulginvinv  19008  subgsubcl  19045  qussub  19098  ghmsub  19131  odhash3  19483  ogrpsublt  20049  srgcom4  20127  dvrcl  20317  unitdvcl  20318  abvsubtri  20737  lspsntrim  21027  frlmsslss2  21707  lindsmm  21760  ascldimul  21820  lply1binomsc  22221  smadiadetglem2  22582  m2cpm  22651  m2cpminvid  22663  pmatcollpwscmat  22701  mp2pm2mp  22721  cpmidgsum  22778  cpmadugsumfi  22787  basgen2  22899  opnneiss  23028  restlp  23093  nmtri  24536  csschl  25298  sincosq1lem  26428  logrec  26695  nosupbnd1lem2  27643  noinfbnd1lem2  27658  noetalem1  27675  grpodivinv  30508  grpoinvdiv  30509  grpodivf  30510  nvmval2  30615  nvaddsub4  30629  nvpi  30639  nvmtri  30643  nvabs  30644  4ipval2  30680  ipval3  30681  isblo2  30755  blof  30757  nmblore  30758  nmlnoubi  30768  nmlnogt0  30769  shsubcl  31192  unopadj  31891  atexch  32353  atcvatlem  32357  ind1  32830  inelsiga  34140  inelros  34178  fineqvnttrclselem3  35135  revpfxsfxrev  35152  mrsubcv  35546  mrsubvr  35547  btwnconn2  36136  ismtybnd  37847  lkrlsp2  39142  opcon2b  39236  opltcon2b  39245  oldmm3N  39258  oldmm4  39259  oldmj3  39262  oldmj4  39263  cmt2N  39289  cmt4N  39291  atleneN  39473  lplnri2N  39593  cdlema2N  39831  pmapojoinN  40007  ltrncnvatb  40177  trlval2  40202  trljat1  40205  cdleme18c  40332  cdleme19c  40344  cdlemeiota  40624  trlcocnv  40759  tendoplco2  40818  cdlemk6  40876  cdlemk7u  40909  cdlemk22  40932  cdlemk24-3  40942  cdlemkid2  40963  cdlemk11ta  40968  cdlemk11tc  40984  cdlemk47  40988  cdlemk52  40993  tendocnv  41060  dibelval1st1  41189  dibelval1st2N  41190  dihord2pre2  41265  mzprename  42782  pell14qrdivcl  42898  pwssplit4  43122  iocmbl  43246  relexpxpmin  43750  dvconstbi  44367  limsupgtlem  45815  dvbdfbdioolem1  45966  ibliccsinexp  45989  stoweidlem22  46060  fourierdlem42  46187  smfsuplem1  46849  divsub1dir  48549