Theorem syld3an3 1406

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 1086

This theorem is referenced by:  brelrng  5930  resin  6845  moriotass  7390  omwordri  8567  oewordri  8587  dif1en  9155  dif1enOLD  9157  sdomdomtrfi  9199  php3  9207  onomeneq  9223  preleqg  9605  gchaleph2  10662  gruf  10801  nnncan1  11492  lediv1  12075  lemuldiv  12090  suprfinzcl  12672  supxrbnd  13303  bcval4  14263  ccatval3  14525  ccatfv0  14529  ccatval1lsw  14530  ccatval21sw  14531  lswccatn0lsw  14537  pfxsuff1eqwrdeq  14645  pfxccatid  14687  cshwidxmodr  14750  2swrd2eqwrdeq  14900  dvdsmultr1  16235  dvdssub2  16240  ndvdsadd  16349  mrcsscl  17560  latnle  18425  latabs1  18427  latabs2  18428  latj4rot  18442  grpsubf  18934  grpinvsub  18937  grpnpcan  18947  mulginvcom  19011  mulginvinv  19012  subgsubcl  19049  qussub  19102  ghmsub  19134  odhash3  19481  srgcom4  20104  dvrcl  20291  unitdvcl  20292  abvsubtri  20663  lspsntrim  20931  frlmsslss2  21630  lindsmm  21683  ascldimul  21742  lply1binomsc  22141  smadiadetglem2  22484  m2cpm  22553  m2cpminvid  22565  pmatcollpwscmat  22603  mp2pm2mp  22623  cpmidgsum  22680  cpmadugsumfi  22689  basgen2  22802  opnneiss  22932  restlp  22997  nmtri  24445  csschl  25214  sincosq1lem  26337  logrec  26599  nosupbnd1lem2  27546  noinfbnd1lem2  27561  noetalem1  27578  grpodivinv  30213  grpoinvdiv  30214  grpodivf  30215  nvmval2  30320  nvaddsub4  30334  nvpi  30344  nvmtri  30348  nvabs  30349  4ipval2  30385  ipval3  30386  isblo2  30460  blof  30462  nmblore  30463  nmlnoubi  30473  nmlnogt0  30474  shsubcl  30897  unopadj  31596  atexch  32058  atcvatlem  32062  ogrpsublt  32666  ind1  33470  inelsiga  33588  inelros  33626  revpfxsfxrev  34561  mrsubcv  34956  mrsubvr  34957  btwnconn2  35535  ismtybnd  37131  lkrlsp2  38429  opcon2b  38523  opltcon2b  38532  oldmm3N  38545  oldmm4  38546  oldmj3  38549  oldmj4  38550  cmt2N  38576  cmt4N  38578  atleneN  38761  lplnri2N  38881  cdlema2N  39119  pmapojoinN  39295  ltrncnvatb  39465  trlval2  39490  trljat1  39493  cdleme18c  39620  cdleme19c  39632  cdlemeiota  39912  trlcocnv  40047  tendoplco2  40106  cdlemk6  40164  cdlemk7u  40197  cdlemk22  40220  cdlemk24-3  40230  cdlemkid2  40251  cdlemk11ta  40256  cdlemk11tc  40272  cdlemk47  40276  cdlemk52  40281  tendocnv  40348  dibelval1st1  40477  dibelval1st2N  40478  dihord2pre2  40553  mzprename  41942  pell14qrdivcl  42058  pwssplit4  42286  iocmbl  42417  relexpxpmin  42923  dvconstbi  43548  limsupgtlem  44944  dvbdfbdioolem1  45095  ibliccsinexp  45118  stoweidlem22  45189  fourierdlem42  45316  smfsuplem1  45978  divsub1dir  47352