Theorem sylibrd 262

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibrd.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
sylibrd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 251	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr4d  297  sbciegft  3721  opeldmd  5760  elreldm  5789  ordtr2  6235  ssimaex  6774  fliftfun  7099  isopolem  7132  isosolem  7134  ordsucss  7575  f1oweALT  7723  fnse  7878  brtpos  7955  issmo2  8064  seqomlem1  8164  omcl  8241  oecl  8242  oawordeulem  8260  oaass  8267  omordi  8272  omord  8274  odi  8285  oen0  8292  oeordi  8293  oeordsuc  8300  nnmcl  8318  nnecl  8319  nnmordi  8337  nnmord  8338  nnmwordri  8342  nnaordex  8344  swoord1  8400  ecopovtrn  8480  f1domg  8626  pw2f1olem  8727  domtriord  8770  mapen  8788  mapxpen  8790  mapunen  8793  nndomog  8815  inficl  9019  supmo  9046  infmo  9089  inf3lem6  9226  cantnflem1  9282  tcmin  9335  tcrank  9465  cardne  9546  cardlim  9553  cardsdomel  9555  carduni  9562  alephord  9654  cardinfima  9676  dfac5lem4  9705  infdif2  9789  cofsmo  9848  cfcoflem  9851  infpssrlem4  9885  infpssrlem5  9886  fin4en1  9888  isfin2-2  9898  enfin2i  9900  fin23lem27  9907  isf32lem12  9943  isf34lem6  9959  domtriomlem  10021  cardmin  10143  fpwwe2lem11  10220  inar1  10354  gruiun  10378  ltsonq  10548  prub  10573  reclem3pr  10628  mulcmpblnr  10650  mulgt0sr  10684  axpre-sup  10748  leltadd  11281  infm3  11756  peano5nni  11798  zextle  12215  prime  12223  uzin  12439  ublbneg  12494  zbtwnre  12507  mul2lt0bi  12657  xrre2  12725  xralrple  12760  xmulneg1  12824  supxrbnd  12883  supxrgtmnf  12884  fzrevral  13162  flge  13345  ceile  13387  modadd1  13446  modmul1  13462  modsumfzodifsn  13482  seqcl2  13559  facdiv  13818  hashss  13941  hash2exprb  14002  elfzelfzccat  14102  repswswrd  14314  cshf1  14340  cshwcsh2id  14358  rlim2lt  15023  rlim3  15024  o1lo1  15063  climshftlem  15100  o1co  15112  o1of2  15139  isercolllem2  15194  isercoll  15196  caucvgrlem2  15203  climcndslem2  15377  sqrt2irr  15773  dvds2lem  15793  dvdsle  15834  dvdsfac  15850  ltoddhalfle  15885  divalglem0  15917  ndvdsadd  15934  bitsinv1lem  15963  sadcaddlem  15979  dvdslegcd  16026  bezoutlem2  16063  bezoutlem4  16065  gcdzeq  16077  algcvga  16099  rpdvds  16180  cncongr1  16187  cncongr2  16188  prmind2  16205  isprm6  16234  rpexp  16242  eulerthlem2  16298  pclem  16354  pceulem  16361  pc2dvds  16395  fldivp1  16413  infpnlem1  16426  prmunb  16430  mrieqv2d  17096  plttr  17802  clatl  17968  issubg4  18516  gexdvds  18927  pgpssslw  18957  sylow2alem2  18961  efgs1b  19080  efgsfo  19083  lspindpi  20123  psgnodpm  20504  psgndif  20518  obselocv  20644  pf1ind  21225  mdetunilem9  21471  fiinbas  21803  bastg  21817  tgcl  21820  opnssneib  21966  clslp  21999  tgcnp  22104  iscnp4  22114  cncls2  22124  cncls  22125  cnntr  22126  cnpresti  22139  lmss  22149  lmcnp  22155  cmpsub  22251  tgcmp  22252  dfconn2  22270  t1connperf  22287  1stcfb  22296  1stcrest  22304  kgenss  22394  llycmpkgen2  22401  txdis  22483  qtoptop2  22550  kqt0lem  22587  isr0  22588  regr1lem2  22591  cmphaushmeo  22651  fbun  22691  ssfg  22723  fgtr  22741  ufildr  22782  cnpflf  22852  fclsnei  22870  flimfnfcls  22879  fclscmp  22881  ufilcmp  22883  cnpfcf  22892  alexsublem  22895  alexsubALTlem3  22900  alexsubALTlem4  22901  ptcmplem3  22905  tgphaus  22968  tgpt1  22969  tsmsres  22995  imasdsf1olem  23225  xblss2ps  23253  xblss2  23254  blsscls2  23356  metequiv2  23362  stdbdxmet  23367  nmoi  23580  reconn  23679  mulc1cncf  23756  cncfco  23758  iccpnfhmeo  23796  xrhmeo  23797  evth  23810  pi1grplem  23900  fgcfil  24122  ivthlem2  24303  ivthlem3  24304  ovolicc2lem4  24371  voliunlem1  24401  ioombl1lem4  24412  itg2gt0  24612  limcco  24744  lhop1  24865  tdeglem4  24911  tdeglem4OLD  24912  plypf1  25060  coeeulem  25072  coeidlem  25085  coeid3  25088  plymul0or  25128  dvnply2  25134  plydivex  25144  vieta1lem2  25158  plyexmo  25160  aaliou3lem2  25190  ulmss  25243  ulmdvlem3  25248  iblulm  25253  sincosq2sgn  25343  sincosq3sgn  25344  sincosq4sgn  25345  logcnlem5  25488  dcubic  25683  amgm  25827  isnsqf  25971  mumullem2  26016  chtublem  26046  chtub  26047  fsumvma2  26049  vmasum  26051  dchrfi  26090  bposlem1  26119  bposlem3  26121  bposlem7  26125  lgsdir  26167  lgsquadlem2  26216  2sqlem8a  26260  2sqlem10  26263  dchrisum0flb  26345  pntpbnd1  26421  pntlemf  26440  pntlem3  26444  axeuclid  27008  uspgrushgr  27220  uspgrupgr  27221  usgruspgr  27223  usgr2pth  27805  crctcshwlkn0lem5  27852  wwlksnext  27931  wwlksnextsurj  27938  clwwlkccatlem  28026  clwlkclwwlkf  28045  clwwisshclwwslemlem  28050  lnon0  28833  normpyc  29181  ocsh  29318  ocorth  29326  ococss  29328  shsel2  29357  hsupss  29376  pjhth  29428  shlub  29449  cm2j  29655  lnfncnbd  30092  riesz1  30100  rnbra  30142  leopadd  30167  leopmuli  30168  hstles  30266  stge1i  30273  stle0i  30274  dmdbr5  30343  ssmd2  30347  superpos  30389  chcv1  30390  atoml2i  30418  chirredlem2  30426  atcvat3i  30431  mdsymlem5  30442  mdsymlem6  30443  sumdmdii  30450  sumdmdlem2  30454  isarchiofld  31189  sqsscirc2  31527  cnre2csqlem  31528  xrge0iifiso  31553  sigaclci  31766  omssubadd  31933  eulerpartlemb  32001  ballotlemimin  32138  ballotlem7  32168  fineqvac  32733  subgrwlk  32761  cusgracyclt3v  32785  cvmlift2lem12  32943  fmlasucdisj  33028  dfon2lem8  33436  soseq  33483  segconeq  33998  ifscgr  34032  brofs2  34065  brifs2  34066  endofsegid  34073  dissneqlem  35197  rdgellim  35233  fvineqsneq  35269  tan2h  35455  matunitlindflem2  35460  poimirlem31  35494  poimir  35496  fzmul  35585  fdc  35589  incsequz2  35593  sstotbnd2  35618  sstotbnd3  35620  totbndbnd  35633  isexid2  35699  ispridl2  35882  mpobi123f  36006  riotasvd  36656  lsator0sp  36701  lssatle  36715  lshpset2N  36819  lkrlspeqN  36871  omllaw2N  36944  cmtbr3N  36954  lecmtN  36956  cvlcvr1  37039  cvrval4N  37114  cvrat3  37142  3noncolr2  37149  4noncolr3  37153  3dimlem3  37161  3dimlem3OLDN  37162  3dimlem4  37164  3dimlem4OLDN  37165  llncvrlpln  37258  lplncvrlvol  37316  snatpsubN  37450  linepsubN  37452  pmapjat1  37553  pclfinclN  37650  pl42N  37683  ltrneq2  37848  cdleme7aa  37942  cdleme18d  37995  cdleme21b  38026  trlord  38269  trlcoat  38423  dochkrshp  39086  lcfl8  39202  mulgt0con1dlem  40076  irrapxlem2  40289  pell14qrdich  40335  monotoddzz  40409  pw2f1ocnv  40503  iocinico  40687  harval3  40769  sbcim2g  41772  stoweidlem62  43221  elfzelfzlble  44429  1arymaptf1  45604  2arymaptf1  45615  eenglngeehlnmlem2  45700  mpbiran3d  45758  opnneil  45819