Theorem syld3an3 1409

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 1371	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  brelrng  5940  resin  6855  moriotass  7400  omwordri  8574  oewordri  8594  dif1en  9162  dif1enOLD  9164  sdomdomtrfi  9206  php3  9214  onomeneq  9230  preleqg  9612  gchaleph2  10669  gruf  10808  nnncan1  11498  lediv1  12081  lemuldiv  12096  suprfinzcl  12678  supxrbnd  13309  bcval4  14269  ccatval3  14531  ccatfv0  14535  ccatval1lsw  14536  ccatval21sw  14537  lswccatn0lsw  14543  pfxsuff1eqwrdeq  14651  pfxccatid  14693  cshwidxmodr  14756  2swrd2eqwrdeq  14906  dvdsmultr1  16241  dvdssub2  16246  ndvdsadd  16355  mrcsscl  17566  latnle  18428  latabs1  18430  latabs2  18431  latj4rot  18445  grpsubf  18904  grpinvsub  18907  grpnpcan  18917  mulginvcom  18981  mulginvinv  18982  subgsubcl  19019  qussub  19072  ghmsub  19102  odhash3  19446  srgcom4  20039  dvrcl  20222  unitdvcl  20223  abvsubtri  20447  lspsntrim  20714  frlmsslss2  21336  lindsmm  21389  ascldimul  21448  lply1binomsc  21838  smadiadetglem2  22181  m2cpm  22250  m2cpminvid  22262  pmatcollpwscmat  22300  mp2pm2mp  22320  cpmidgsum  22377  cpmadugsumfi  22386  basgen2  22499  opnneiss  22629  restlp  22694  nmtri  24142  csschl  24900  sincosq1lem  26014  logrec  26275  nosupbnd1lem2  27219  noinfbnd1lem2  27234  noetalem1  27251  grpodivinv  29827  grpoinvdiv  29828  grpodivf  29829  nvmval2  29934  nvaddsub4  29948  nvpi  29958  nvmtri  29962  nvabs  29963  4ipval2  29999  ipval3  30000  isblo2  30074  blof  30076  nmblore  30077  nmlnoubi  30087  nmlnogt0  30088  shsubcl  30511  unopadj  31210  atexch  31672  atcvatlem  31676  ogrpsublt  32280  ind1  33084  inelsiga  33202  inelros  33240  revpfxsfxrev  34175  mrsubcv  34570  mrsubvr  34571  btwnconn2  35143  ismtybnd  36761  lkrlsp2  38059  opcon2b  38153  opltcon2b  38162  oldmm3N  38175  oldmm4  38176  oldmj3  38179  oldmj4  38180  cmt2N  38206  cmt4N  38208  atleneN  38391  lplnri2N  38511  cdlema2N  38749  pmapojoinN  38925  ltrncnvatb  39095  trlval2  39120  trljat1  39123  cdleme18c  39250  cdleme19c  39262  cdlemeiota  39542  trlcocnv  39677  tendoplco2  39736  cdlemk6  39794  cdlemk7u  39827  cdlemk22  39850  cdlemk24-3  39860  cdlemkid2  39881  cdlemk11ta  39886  cdlemk11tc  39902  cdlemk47  39906  cdlemk52  39911  tendocnv  39978  dibelval1st1  40107  dibelval1st2N  40108  dihord2pre2  40183  mzprename  41569  pell14qrdivcl  41685  pwssplit4  41913  iocmbl  42044  relexpxpmin  42550  dvconstbi  43175  limsupgtlem  44572  dvbdfbdioolem1  44723  ibliccsinexp  44746  stoweidlem22  44817  fourierdlem42  44944  smfsuplem1  45606  divsub1dir  47276