Theorem syld3an3 1412

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 1374	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  5896  resin  6802  moriotass  7356  omwordri  8507  oewordri  8528  dif1en  9096  sdomdomtrfi  9135  php3  9143  onomeneq  9148  preleqg  9536  gchaleph2  10595  gruf  10734  nnncan1  11430  lediv1  12021  lemuldiv  12036  ind1  12168  suprfinzcl  12643  supxrbnd  13280  bcval4  14269  ccatval3  14541  ccatfv0  14546  ccatval1lsw  14547  ccatval21sw  14548  lswccatn0lsw  14554  pfxsuff1eqwrdeq  14661  pfxccatid  14703  cshwidxmodr  14766  2swrd2eqwrdeq  14915  dvdsmultr1  16265  dvdssub2  16270  ndvdsadd  16379  mrcsscl  17586  latnle  18439  latabs1  18441  latabs2  18442  latj4rot  18456  grpsubf  18995  grpinvsub  18998  grpnpcan  19008  mulginvcom  19075  mulginvinv  19076  subgsubcl  19113  qussub  19166  ghmsub  19199  odhash3  19551  ogrpsublt  20117  srgcom4  20195  dvrcl  20384  unitdvcl  20385  abvsubtri  20804  lspsntrim  21093  frlmsslss2  21755  lindsmm  21808  ascldimul  21868  lply1binomsc  22276  smadiadetglem2  22637  m2cpm  22706  m2cpminvid  22718  pmatcollpwscmat  22756  mp2pm2mp  22776  cpmidgsum  22833  cpmadugsumfi  22842  basgen2  22954  opnneiss  23083  restlp  23148  nmtri  24591  csschl  25343  sincosq1lem  26461  logrec  26727  nosupbnd1lem2  27673  noinfbnd1lem2  27688  noetalem1  27705  grpodivinv  30607  grpoinvdiv  30608  grpodivf  30609  nvmval2  30714  nvaddsub4  30728  nvpi  30738  nvmtri  30742  nvabs  30743  4ipval2  30779  ipval3  30780  isblo2  30854  blof  30856  nmblore  30857  nmlnoubi  30867  nmlnogt0  30868  shsubcl  31291  unopadj  31990  atexch  32452  atcvatlem  32456  inelsiga  34279  inelros  34317  fineqvnttrclselem3  35267  revpfxsfxrev  35298  mrsubcv  35692  mrsubvr  35693  btwnconn2  36284  ismtybnd  38128  lkrlsp2  39549  opcon2b  39643  opltcon2b  39652  oldmm3N  39665  oldmm4  39666  oldmj3  39669  oldmj4  39670  cmt2N  39696  cmt4N  39698  atleneN  39880  lplnri2N  40000  cdlema2N  40238  pmapojoinN  40414  ltrncnvatb  40584  trlval2  40609  trljat1  40612  cdleme18c  40739  cdleme19c  40751  cdlemeiota  41031  trlcocnv  41166  tendoplco2  41225  cdlemk6  41283  cdlemk7u  41316  cdlemk22  41339  cdlemk24-3  41349  cdlemkid2  41370  cdlemk11ta  41375  cdlemk11tc  41391  cdlemk47  41395  cdlemk52  41400  tendocnv  41467  dibelval1st1  41596  dibelval1st2N  41597  dihord2pre2  41672  mzprename  43181  pell14qrdivcl  43293  pwssplit4  43517  iocmbl  43641  relexpxpmin  44144  dvconstbi  44761  limsupgtlem  46205  dvbdfbdioolem1  46356  ibliccsinexp  46379  stoweidlem22  46450  fourierdlem42  46577  smfsuplem1  47239  divsub1dir  48993