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  5890  resin  6796  moriotass  7349  omwordri  8500  oewordri  8521  dif1en  9089  sdomdomtrfi  9128  php3  9136  onomeneq  9141  preleqg  9527  gchaleph2  10586  gruf  10725  nnncan1  11421  lediv1  12012  lemuldiv  12027  ind1  12159  suprfinzcl  12634  supxrbnd  13271  bcval4  14260  ccatval3  14532  ccatfv0  14537  ccatval1lsw  14538  ccatval21sw  14539  lswccatn0lsw  14545  pfxsuff1eqwrdeq  14652  pfxccatid  14694  cshwidxmodr  14757  2swrd2eqwrdeq  14906  dvdsmultr1  16256  dvdssub2  16261  ndvdsadd  16370  mrcsscl  17577  latnle  18430  latabs1  18432  latabs2  18433  latj4rot  18447  grpsubf  18986  grpinvsub  18989  grpnpcan  18999  mulginvcom  19066  mulginvinv  19067  subgsubcl  19104  qussub  19157  ghmsub  19190  odhash3  19542  ogrpsublt  20108  srgcom4  20186  dvrcl  20375  unitdvcl  20376  abvsubtri  20795  lspsntrim  21085  frlmsslss2  21765  lindsmm  21818  ascldimul  21878  lply1binomsc  22286  smadiadetglem2  22647  m2cpm  22716  m2cpminvid  22728  pmatcollpwscmat  22766  mp2pm2mp  22786  cpmidgsum  22843  cpmadugsumfi  22852  basgen2  22964  opnneiss  23093  restlp  23158  nmtri  24601  csschl  25353  sincosq1lem  26474  logrec  26740  nosupbnd1lem2  27687  noinfbnd1lem2  27702  noetalem1  27719  grpodivinv  30622  grpoinvdiv  30623  grpodivf  30624  nvmval2  30729  nvaddsub4  30743  nvpi  30753  nvmtri  30757  nvabs  30758  4ipval2  30794  ipval3  30795  isblo2  30869  blof  30871  nmblore  30872  nmlnoubi  30882  nmlnogt0  30883  shsubcl  31306  unopadj  32005  atexch  32467  atcvatlem  32471  inelsiga  34295  inelros  34333  fineqvnttrclselem3  35283  revpfxsfxrev  35314  mrsubcv  35708  mrsubvr  35709  btwnconn2  36300  ismtybnd  38142  lkrlsp2  39563  opcon2b  39657  opltcon2b  39666  oldmm3N  39679  oldmm4  39680  oldmj3  39683  oldmj4  39684  cmt2N  39710  cmt4N  39712  atleneN  39894  lplnri2N  40014  cdlema2N  40252  pmapojoinN  40428  ltrncnvatb  40598  trlval2  40623  trljat1  40626  cdleme18c  40753  cdleme19c  40765  cdlemeiota  41045  trlcocnv  41180  tendoplco2  41239  cdlemk6  41297  cdlemk7u  41330  cdlemk22  41353  cdlemk24-3  41363  cdlemkid2  41384  cdlemk11ta  41389  cdlemk11tc  41405  cdlemk47  41409  cdlemk52  41414  tendocnv  41481  dibelval1st1  41610  dibelval1st2N  41611  dihord2pre2  41686  mzprename  43195  pell14qrdivcl  43311  pwssplit4  43535  iocmbl  43659  relexpxpmin  44162  dvconstbi  44779  limsupgtlem  46223  dvbdfbdioolem1  46374  ibliccsinexp  46397  stoweidlem22  46468  fourierdlem42  46595  smfsuplem1  47257  divsub1dir  49005