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 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2		simp2 1138	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)
3		syld3an3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4		syld3an3.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  brelrng  5952  resin  6870  moriotass  7420  omwordri  8610  oewordri  8630  dif1en  9200  dif1enOLD  9202  sdomdomtrfi  9241  php3  9249  onomeneq  9265  preleqg  9655  gchaleph2  10712  gruf  10851  nnncan1  11545  lediv1  12133  lemuldiv  12148  suprfinzcl  12732  supxrbnd  13370  bcval4  14346  ccatval3  14617  ccatfv0  14621  ccatval1lsw  14622  ccatval21sw  14623  lswccatn0lsw  14629  pfxsuff1eqwrdeq  14737  pfxccatid  14779  cshwidxmodr  14842  2swrd2eqwrdeq  14992  dvdsmultr1  16333  dvdssub2  16338  ndvdsadd  16447  mrcsscl  17663  latnle  18518  latabs1  18520  latabs2  18521  latj4rot  18535  grpsubf  19037  grpinvsub  19040  grpnpcan  19050  mulginvcom  19117  mulginvinv  19118  subgsubcl  19155  qussub  19209  ghmsub  19242  odhash3  19594  srgcom4  20211  dvrcl  20404  unitdvcl  20405  abvsubtri  20828  lspsntrim  21097  frlmsslss2  21795  lindsmm  21848  ascldimul  21908  lply1binomsc  22315  smadiadetglem2  22678  m2cpm  22747  m2cpminvid  22759  pmatcollpwscmat  22797  mp2pm2mp  22817  cpmidgsum  22874  cpmadugsumfi  22883  basgen2  22996  opnneiss  23126  restlp  23191  nmtri  24639  csschl  25410  sincosq1lem  26539  logrec  26806  nosupbnd1lem2  27754  noinfbnd1lem2  27769  noetalem1  27786  grpodivinv  30555  grpoinvdiv  30556  grpodivf  30557  nvmval2  30662  nvaddsub4  30676  nvpi  30686  nvmtri  30690  nvabs  30691  4ipval2  30727  ipval3  30728  isblo2  30802  blof  30804  nmblore  30805  nmlnoubi  30815  nmlnogt0  30816  shsubcl  31239  unopadj  31938  atexch  32400  atcvatlem  32404  ind1  32842  ogrpsublt  33098  inelsiga  34136  inelros  34174  revpfxsfxrev  35121  mrsubcv  35515  mrsubvr  35516  btwnconn2  36103  ismtybnd  37814  lkrlsp2  39104  opcon2b  39198  opltcon2b  39207  oldmm3N  39220  oldmm4  39221  oldmj3  39224  oldmj4  39225  cmt2N  39251  cmt4N  39253  atleneN  39436  lplnri2N  39556  cdlema2N  39794  pmapojoinN  39970  ltrncnvatb  40140  trlval2  40165  trljat1  40168  cdleme18c  40295  cdleme19c  40307  cdlemeiota  40587  trlcocnv  40722  tendoplco2  40781  cdlemk6  40839  cdlemk7u  40872  cdlemk22  40895  cdlemk24-3  40905  cdlemkid2  40926  cdlemk11ta  40931  cdlemk11tc  40947  cdlemk47  40951  cdlemk52  40956  tendocnv  41023  dibelval1st1  41152  dibelval1st2N  41153  dihord2pre2  41228  mzprename  42760  pell14qrdivcl  42876  pwssplit4  43101  iocmbl  43225  relexpxpmin  43730  dvconstbi  44353  limsupgtlem  45792  dvbdfbdioolem1  45943  ibliccsinexp  45966  stoweidlem22  46037  fourierdlem42  46164  smfsuplem1  46826  divsub1dir  48434