Theorem syld3an3 1407

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  brelrng  5839  resin  6721  moriotass  7245  omwordri  8365  oewordri  8385  dif1en  8907  domtrfi  8938  preleqg  9303  gchaleph2  10359  gruf  10498  nnncan1  11187  lediv1  11770  lemuldiv  11785  suprfinzcl  12365  supxrbnd  12991  bcval4  13949  ccatval3  14212  ccatfv0  14216  ccatval1lsw  14217  ccatval21sw  14218  lswccatn0lsw  14224  pfxsuff1eqwrdeq  14340  pfxccatid  14382  cshwidxmodr  14445  2swrd2eqwrdeq  14594  dvdsmultr1  15933  dvdssub2  15938  ndvdsadd  16047  mrcsscl  17246  latnle  18106  latabs1  18108  latabs2  18109  latj4rot  18123  grpsubf  18569  grpinvsub  18572  grpnpcan  18582  mulginvcom  18643  mulginvinv  18644  subgsubcl  18681  qussub  18731  ghmsub  18757  odhash3  19096  dvrcl  19843  unitdvcl  19844  abvsubtri  20010  lspsntrim  20275  frlmsslss2  20892  lindsmm  20945  ascldimul  21002  lply1binomsc  21388  smadiadetglem2  21729  m2cpm  21798  m2cpminvid  21810  pmatcollpwscmat  21848  mp2pm2mp  21868  cpmidgsum  21925  cpmadugsumfi  21934  basgen2  22047  opnneiss  22177  restlp  22242  nmtri  23688  csschl  24445  sincosq1lem  25559  logrec  25818  grpodivinv  28799  grpoinvdiv  28800  grpodivf  28801  nvmval2  28906  nvaddsub4  28920  nvpi  28930  nvmtri  28934  nvabs  28935  4ipval2  28971  ipval3  28972  isblo2  29046  blof  29048  nmblore  29049  nmlnoubi  29059  nmlnogt0  29060  shsubcl  29483  unopadj  30182  atexch  30644  atcvatlem  30648  ogrpsublt  31249  ind1  31885  inelsiga  32003  inelros  32041  revpfxsfxrev  32977  mrsubcv  33372  mrsubvr  33373  nosupbnd1lem2  33839  noinfbnd1lem2  33854  noetalem1  33871  btwnconn2  34331  ismtybnd  35892  lkrlsp2  37044  opcon2b  37138  opltcon2b  37147  oldmm3N  37160  oldmm4  37161  oldmj3  37164  oldmj4  37165  cmt2N  37191  cmt4N  37193  atleneN  37375  lplnri2N  37495  cdlema2N  37733  pmapojoinN  37909  ltrncnvatb  38079  trlval2  38104  trljat1  38107  cdleme18c  38234  cdleme19c  38246  cdlemeiota  38526  trlcocnv  38661  tendoplco2  38720  cdlemk6  38778  cdlemk7u  38811  cdlemk22  38834  cdlemk24-3  38844  cdlemkid2  38865  cdlemk11ta  38870  cdlemk11tc  38886  cdlemk47  38890  cdlemk52  38895  tendocnv  38962  dibelval1st1  39091  dibelval1st2N  39092  dihord2pre2  39167  mzprename  40487  pell14qrdivcl  40603  pwssplit4  40830  iocmbl  40960  relexpxpmin  41214  dvconstbi  41841  limsupgtlem  43208  dvbdfbdioolem1  43359  ibliccsinexp  43382  stoweidlem22  43453  fourierdlem42  43580  smfsuplem1  44231  divsub1dir  45746