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 48	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  opeldmd  5887  elreldm  5916  predtrss  6313  ordtr2  6395  ssimaex  6956  fliftfun  7300  isopolem  7333  isosolem  7335  ordsucss  7802  f1oweALT  7957  fnse  8117  soseq  8143  brtpos  8219  issmo2  8324  seqomlem1  8425  omcl  8509  oecl  8510  oawordeulem  8527  oaass  8534  omordi  8539  omord  8541  odi  8552  oen0  8560  oeordi  8561  oeordsuc  8568  nnmcl  8586  nnecl  8587  nnmordi  8605  nnmord  8606  nnmwordri  8610  nnaordex  8612  swoord1  8715  ecopovtrn  8806  f1domg  8956  pw2f1olem  9057  domtriord  9099  mapen  9117  mapxpen  9119  mapunen  9122  nndomog  9185  onomeneq  9186  inficl  9373  supmo  9400  infmo  9445  inf3lem6  9590  cantnflem1  9646  tcmin  9696  tcrank  9844  cardne  9939  cardlim  9946  cardsdomel  9948  carduni  9955  alephord  10047  cardinfima  10069  dfac5lem4  10098  infdif2  10180  cofsmo  10241  cfcoflem  10244  infpssrlem4  10278  infpssrlem5  10279  fin4en1  10281  isfin2-2  10291  enfin2i  10293  fin23lem27  10300  isf32lem12  10336  isf34lem6  10352  domtriomlem  10414  cardmin  10536  fpwwe2lem11  10614  inar1  10748  gruiun  10772  ltsonq  10942  prub  10967  reclem3pr  11022  mulcmpblnr  11044  mulgt0sr  11078  axpre-sup  11142  leltadd  11686  infm3  12165  peano5nni  12227  zextle  12660  prime  12668  uzin  12889  ublbneg  12948  zbtwnre  12961  mul2lt0bi  13115  xrre2  13187  xralrple  13222  xmulneg1  13286  supxrbnd  13345  supxrgtmnf  13346  fzrevral  13631  flge  13829  ceile  13873  modadd1  13932  modmul1  13951  modsumfzodifsn  13971  seqcl2  14047  facdiv  14314  hashss  14436  hash2exprb  14498  elfzelfzccat  14607  repswswrd  14811  cshf1  14837  cshwcsh2id  14855  rlim2lt  15538  rlim3  15539  o1lo1  15578  climshftlem  15615  o1co  15627  o1of2  15654  isercolllem2  15707  isercoll  15709  caucvgrlem2  15716  climcndslem2  15894  sqrt2irr  16295  dvds2lem  16316  dvdsle  16358  dvdsfac  16374  ltoddhalfle  16409  divalglem0  16441  ndvdsadd  16458  bitsinv1lem  16489  sadcaddlem  16505  dvdslegcd  16552  bezoutlem2  16588  bezoutlem4  16590  gcdzeq  16600  algcvga  16627  rpdvds  16708  cncongr1  16715  cncongr2  16716  prmind2  16733  isprm6  16763  rpexp  16771  eulerthlem2  16831  pclem  16888  pceulem  16895  pc2dvds  16929  fldivp1  16947  infpnlem1  16960  prmunb  16964  mrieqv2d  17685  plttr  18386  clatl  18554  issubg4  19203  gexdvds  19645  pgpssslw  19675  sylow2alem2  19679  efgs1b  19797  efgsfo  19800  imasabl  19937  lspindpi  21225  psgnodpm  21698  psgndif  21712  obselocv  21838  pf1ind  22476  mdetunilem9  22738  fiinbas  23070  bastg  23084  tgcl  23087  opnssneib  23233  clslp  23266  tgcnp  23371  iscnp4  23381  cncls2  23391  cncls  23392  cnntr  23393  cnpresti  23406  lmss  23416  lmcnp  23422  cmpsub  23518  tgcmp  23519  dfconn2  23537  t1connperf  23554  1stcfb  23563  1stcrest  23571  kgenss  23661  llycmpkgen2  23668  txdis  23750  qtoptop2  23817  kqt0lem  23854  isr0  23855  regr1lem2  23858  cmphaushmeo  23918  fbun  23958  ssfg  23990  fgtr  24008  ufildr  24049  cnpflf  24119  fclsnei  24137  flimfnfcls  24146  fclscmp  24148  ufilcmp  24150  cnpfcf  24159  alexsublem  24162  alexsubALTlem3  24167  alexsubALTlem4  24168  ptcmplem3  24172  tgphaus  24235  tgpt1  24236  tsmsres  24262  imasdsf1olem  24491  xblss2ps  24519  xblss2  24520  blsscls2  24622  metequiv2  24628  stdbdxmet  24633  nmoi  24846  reconn  24947  mulc1cncf  25025  cncfco  25027  iccpnfhmeo  25065  xrhmeo  25066  evth  25079  pi1grplem  25169  fgcfil  25391  ivthlem2  25572  ivthlem3  25573  ovolicc2lem4  25640  voliunlem1  25670  ioombl1lem4  25681  itg2gt0  25880  limcco  26013  lhop1  26134  tdeglem4  26178  plypf1  26330  coeeulem  26342  coeidlem  26355  coeid3  26358  plymul0or  26400  dvnply2  26409  plydivex  26419  vieta1lem2  26433  plyexmo  26435  aaliou3lem2  26465  ulmss  26518  ulmdvlem3  26523  iblulm  26528  sincosq2sgn  26622  sincosq3sgn  26623  sincosq4sgn  26624  logcnlem5  26769  dcubic  26969  amgm  27113  isnsqf  27257  mumullem2  27302  chtublem  27333  chtub  27334  fsumvma2  27336  vmasum  27338  dchrfi  27377  bposlem1  27406  bposlem3  27408  bposlem7  27412  lgsdir  27454  lgsquadlem2  27503  2sqlem8a  27547  2sqlem10  27550  dchrisum0flb  27632  pntpbnd1  27708  pntlemf  27727  pntlem3  27731  addonbday  28430  peano5uzs  28555  axeuclid  29222  uspgrushgr  29436  uspgrupgr  29437  usgruspgr  29439  usgr2pth  30022  crctcshwlkn0lem5  30072  wwlksnext  30151  wwlksnextsurj  30158  clwwlkccatlem  30249  clwlkclwwlkf  30268  clwwisshclwwslemlem  30273  lnon0  31059  normpyc  31407  ocsh  31544  ocorth  31552  ococss  31554  shsel2  31583  hsupss  31602  pjhth  31654  shlub  31675  cm2j  31881  lnfncnbd  32318  riesz1  32326  rnbra  32368  leopadd  32393  leopmuli  32394  hstles  32492  stge1i  32499  stle0i  32500  dmdbr5  32569  ssmd2  32573  superpos  32615  chcv1  32616  atoml2i  32644  chirredlem2  32652  atcvat3i  32657  mdsymlem5  32668  mdsymlem6  32669  sumdmdii  32676  sumdmdlem2  32680  isarchiofld  33432  sqsscirc2  34216  cnre2csqlem  34217  xrge0iifiso  34242  sigaclci  34439  omssubadd  34607  eulerpartlemb  34675  ballotlemimin  34813  ballotlem7  34843  fineqvac  35424  fineqvinfep  35433  vonf1wev  35463  vonf1owevOLD  35465  subgrwlk  35495  cusgracyclt3v  35519  cvmlift2lem12  35677  fmlasucdisj  35762  dfon2lem8  36151  segconeq  36373  ifscgr  36407  brofs2  36440  brifs2  36441  endofsegid  36448  dissneqlem  37846  rdgellim  37882  fvineqsneq  37918  tan2h  38123  matunitlindflem2  38128  poimirlem31  38162  poimir  38164  fzmul  38252  fdc  38256  incsequz2  38260  sstotbnd2  38285  sstotbnd3  38287  totbndbnd  38300  isexid2  38366  ispridl2  38549  mpobi123f  38673  disjlem18  39414  disjdmqsss  39416  eldisjs6  39451  riotasvd  39592  lsator0sp  39637  lssatle  39651  lshpset2N  39755  lkrlspeqN  39807  omllaw2N  39880  cmtbr3N  39890  lecmtN  39892  cvlcvr1  39975  cvrval4N  40050  cvrat3  40078  3noncolr2  40085  4noncolr3  40089  3dimlem3  40097  3dimlem3OLDN  40098  3dimlem4  40100  3dimlem4OLDN  40101  llncvrlpln  40194  lplncvrlvol  40252  snatpsubN  40386  linepsubN  40388  pmapjat1  40489  pclfinclN  40586  pl42N  40619  ltrneq2  40784  cdleme7aa  40878  cdleme18d  40931  cdleme21b  40962  trlord  41205  trlcoat  41359  dochkrshp  42022  lcfl8  42138  mulgt0con1dlem  43103  irrapxlem2  43412  pell14qrdich  43458  monotoddzz  43532  pw2f1ocnv  43626  iocinico  43801  ordnexbtwnsuc  43856  tfsconcat0i  43934  naddwordnexlem4  43990  harval3  44126  sbcim2g  45112  stoweidlem62  46634  elfzelfzlble  47913  pgnbgreunbgrlem1  48733  pgnbgreunbgrlem4  48739  1arymaptf1  49273  2arymaptf1  49284  eenglngeehlnmlem2  49369  mpbiran3d  49426  opnneil  49539