Theorem syld3an3 1436

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  brelrng  5924  resin  6852  moriotass  7413  omwordri  8587  oewordri  8608  dif1en  9184  sdomdomtrfi  9223  php3  9231  onomeneq  9236  preleqg  9623  gchaleph2  10764  gruf  10903  nnncan1  11601  lediv1  12189  lemuldiv  12204  ind1  12336  suprfinzcl  12820  supxrbnd  13465  bcval4  14458  ccatval3  14731  ccatfv0  14736  ccatval1lsw  14737  ccatval21sw  14738  lswccatn0lsw  14745  pfxsuff1eqwrdeq  14856  pfxccatid  14898  revpfxsfxrev  14925  cshwidxmodr  14963  2swrd2eqwrdeq  15115  dvdsmultr1  16475  dvdssub2  16480  ndvdsadd  16589  mrcsscl  17803  latnle  18656  latabs1  18658  latabs2  18659  latj4rot  18673  grpsubf  19238  grpinvsub  19241  grpnpcan  19251  mulginvcom  19318  mulginvinv  19319  subgsubcl  19357  qussub  19415  ghmsub  19447  odhash3  19799  ogrpsublt  20365  srgcom4  20449  dvrcl  20643  unitdvcl  20644  abvsubtri  21093  lspsntrim  21382  frlmsslss2  22090  lindsmm  22143  ascldimul  22205  lply1binomsc  22638  smadiadetglem2  22996  m2cpm  23068  m2cpminvid  23080  pmatcollpwscmat  23118  mp2pm2mp  23138  cpmidgsum  23195  cpmadugsumfi  23204  basgen2  23316  opnneiss  23445  restlp  23510  nmtri  24954  csschl  25706  sincosq1lem  26835  logrec  27100  nosupbnd1lem2  28075  noinfbnd1lem2  28090  noetalem1  28107  grpodivinv  31147  grpoinvdiv  31148  grpodivf  31149  nvmval2  31254  nvaddsub4  31268  nvpi  31278  nvmtri  31282  nvabs  31283  4ipval2  31319  ipval3  31320  isblo2  31394  blof  31396  nmblore  31397  nmlnoubi  31407  nmlnogt0  31408  shsubcl  31831  unopadj  32530  atexch  32992  atcvatlem  32996  inelsiga  34818  inelros  34856  fineqvnttrclselem3  35851  mrsubcv  36365  mrsubvr  36366  btwnconn2  36963  ismtybnd  38850  lkrlsp2  40269  opcon2b  40363  opltcon2b  40372  oldmm3N  40385  oldmm4  40386  oldmj3  40389  oldmj4  40390  cmt2N  40416  cmt4N  40418  atleneN  40600  lplnri2N  40720  cdlema2N  40958  pmapojoinN  41134  ltrncnvatb  41304  trlval2  41329  trljat1  41332  cdleme18c  41459  cdleme19c  41471  cdlemeiota  41751  trlcocnv  41886  tendoplco2  41945  cdlemk6  42003  cdlemk7u  42036  cdlemk22  42059  cdlemk24-3  42069  cdlemkid2  42090  cdlemk11ta  42095  cdlemk11tc  42111  cdlemk47  42115  cdlemk52  42120  tendocnv  42187  dibelval1st1  42316  dibelval1st2N  42317  dihord2pre2  42392  mzprename  43869  pell14qrdivcl  43981  pwssplit4  44200  iocmbl  44324  relexpxpmin  44826  dvconstbi  45427  limsupgtlem  46895  dvbdfbdioolem1  47046  ibliccsinexp  47069  stoweidlem22  47140  fourierdlem42  47267  smfsuplem1  47929  divsub1dir  49737