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  5921  resin  6840  moriotass  7394  omwordri  8584  oewordri  8604  dif1en  9174  dif1enOLD  9176  sdomdomtrfi  9215  php3  9223  onomeneq  9237  preleqg  9629  gchaleph2  10686  gruf  10825  nnncan1  11519  lediv1  12107  lemuldiv  12122  suprfinzcl  12707  supxrbnd  13344  bcval4  14325  ccatval3  14597  ccatfv0  14601  ccatval1lsw  14602  ccatval21sw  14603  lswccatn0lsw  14609  pfxsuff1eqwrdeq  14717  pfxccatid  14759  cshwidxmodr  14822  2swrd2eqwrdeq  14972  dvdsmultr1  16315  dvdssub2  16320  ndvdsadd  16429  mrcsscl  17632  latnle  18483  latabs1  18485  latabs2  18486  latj4rot  18500  grpsubf  19002  grpinvsub  19005  grpnpcan  19015  mulginvcom  19082  mulginvinv  19083  subgsubcl  19120  qussub  19174  ghmsub  19207  odhash3  19557  srgcom4  20174  dvrcl  20364  unitdvcl  20365  abvsubtri  20787  lspsntrim  21056  frlmsslss2  21735  lindsmm  21788  ascldimul  21848  lply1binomsc  22249  smadiadetglem2  22610  m2cpm  22679  m2cpminvid  22691  pmatcollpwscmat  22729  mp2pm2mp  22749  cpmidgsum  22806  cpmadugsumfi  22815  basgen2  22927  opnneiss  23056  restlp  23121  nmtri  24565  csschl  25328  sincosq1lem  26458  logrec  26725  nosupbnd1lem2  27673  noinfbnd1lem2  27688  noetalem1  27705  grpodivinv  30517  grpoinvdiv  30518  grpodivf  30519  nvmval2  30624  nvaddsub4  30638  nvpi  30648  nvmtri  30652  nvabs  30653  4ipval2  30689  ipval3  30690  isblo2  30764  blof  30766  nmblore  30767  nmlnoubi  30777  nmlnogt0  30778  shsubcl  31201  unopadj  31900  atexch  32362  atcvatlem  32366  ind1  32834  ogrpsublt  33089  inelsiga  34166  inelros  34204  revpfxsfxrev  35138  mrsubcv  35532  mrsubvr  35533  btwnconn2  36120  ismtybnd  37831  lkrlsp2  39121  opcon2b  39215  opltcon2b  39224  oldmm3N  39237  oldmm4  39238  oldmj3  39241  oldmj4  39242  cmt2N  39268  cmt4N  39270  atleneN  39453  lplnri2N  39573  cdlema2N  39811  pmapojoinN  39987  ltrncnvatb  40157  trlval2  40182  trljat1  40185  cdleme18c  40312  cdleme19c  40324  cdlemeiota  40604  trlcocnv  40739  tendoplco2  40798  cdlemk6  40856  cdlemk7u  40889  cdlemk22  40912  cdlemk24-3  40922  cdlemkid2  40943  cdlemk11ta  40948  cdlemk11tc  40964  cdlemk47  40968  cdlemk52  40973  tendocnv  41040  dibelval1st1  41169  dibelval1st2N  41170  dihord2pre2  41245  mzprename  42772  pell14qrdivcl  42888  pwssplit4  43113  iocmbl  43237  relexpxpmin  43741  dvconstbi  44358  limsupgtlem  45806  dvbdfbdioolem1  45957  ibliccsinexp  45980  stoweidlem22  46051  fourierdlem42  46178  smfsuplem1  46840  divsub1dir  48493