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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

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

This theorem is used by:  3imtr4d  297  opeldmd  5884  elreldm  5913  predtrss  6314  ordtr2  6397  ssimaex  6958  fliftfun  7308  isopolem  7341  isosolem  7343  f1we  7351  ordsucss  7812  f1oweALT  7967  fnse  8128  soseq  8154  brtpos  8230  issmo2  8335  onelfvnef1  8427  seqomlem1  8438  omcl  8522  oecl  8523  oawordeulem  8540  oaass  8547  omordi  8552  omord  8554  odi  8565  oen0  8573  oeordi  8574  oeordsuc  8581  nnmcl  8599  nnecl  8600  nnmordi  8618  nnmord  8619  nnmwordri  8623  nnaordex  8625  swoord1  8728  ecopovtrn  8819  f1domg  8976  pw2f1olem  9078  domtriord  9120  mapen  9138  mapxpen  9140  mapunen  9143  nndomog  9206  onomeneq  9207  inficl  9395  supmo  9422  infmo  9467  inf3lem6  9612  cantnflem1  9668  tcmin  9718  tcrank  9874  cardne  10018  cardlim  10025  cardsdomel  10027  carduni  10034  alephord  10126  cardinfima  10148  dfac5lem4  10177  infdif2  10259  cofsmo  10319  cfcoflem  10322  infpssrlem4  10356  infpssrlem5  10357  fin4en1  10359  isfin2-2  10369  enfin2i  10371  fin23lem27  10378  isf32lem12  10414  isf34lem6  10430  domtriomlem  10492  cardmin  10620  fpwwe2lem11  10698  inar1  10832  gruiun  10856  ltsonq  11026  prub  11051  reclem3pr  11106  mulcmpblnr  11128  mulgt0sr  11162  axpre-sup  11226  leltadd  11770  infm3  12246  peano5nni  12308  zextle  12742  prime  12750  uzin  12971  ublbneg  13030  zbtwnre  13043  mul2lt0bi  13198  xrre2  13270  xralrple  13305  xmulneg1  13369  supxrbnd  13428  supxrgtmnf  13429  fzrevral  13715  flge  13914  ceile  13958  modadd1  14017  modmul1  14036  modsumfzodifsn  14056  seqcl2  14132  facdiv  14399  hashss  14521  hash2exprb  14584  elfzelfzccat  14693  repswswrd  14903  cshf1  14929  cshwcsh2id  14947  rlim2lt  15632  rlim3  15633  o1lo1  15672  climshftlem  15709  o1co  15721  o1of2  15748  isercolllem2  15801  isercoll  15803  caucvgrlem2  15810  climcndslem2  15987  sqrt2irr  16385  dvds2lem  16406  dvdsle  16448  dvdsfac  16464  ltoddhalfle  16499  divalglem0  16531  ndvdsadd  16548  bitsinv1lem  16579  sadcaddlem  16595  dvdslegcd  16642  bezoutlem2  16678  bezoutlem4  16680  gcdzeq  16690  algcvga  16717  rpdvds  16798  cncongr1  16805  cncongr2  16806  prmind2  16823  isprm6  16853  rpexp  16861  eulerthlem2  16921  pclem  16978  pceulem  16985  pc2dvds  17019  fldivp1  17037  infpnlem1  17050  prmunb  17054  mrieqv2d  17775  plttr  18476  clatl  18644  idressidex0  18822  issubg4  19318  gexdvds  19760  pgpssslw  19790  sylow2alem2  19794  efgs1b  19912  efgsfo  19915  imasabl  20052  lspindpi  21372  psgnodpm  21856  psgndif  21870  obselocv  21996  pf1ind  22635  mdetunilem9  22897  matunitlindflem2  22957  fiinbas  23232  bastg  23246  tgcl  23249  opnssneib  23395  clslp  23428  tgcnp  23533  iscnp4  23543  cncls2  23553  cncls  23554  cnntr  23555  cnpresti  23568  lmss  23578  lmcnp  23584  cmpsub  23680  tgcmp  23681  dfconn2  23699  t1connperf  23716  1stcfb  23725  1stcrest  23733  kgenss  23824  llycmpkgen2  23831  txdis  23913  qtoptop2  23980  kqt0lem  24017  isr0  24018  regr1lem2  24021  cmphaushmeo  24081  fbun  24121  ssfg  24153  fgtr  24171  ufildr  24212  cnpflf  24282  fclsnei  24300  flimfnfcls  24309  fclscmp  24311  ufilcmp  24313  cnpfcf  24322  alexsublem  24325  alexsubALTlem3  24330  alexsubALTlem4  24331  ptcmplem3  24335  tgphaus  24398  tgpt1  24399  tsmsres  24425  imasdsf1olem  24654  xblss2ps  24682  xblss2  24683  blsscls2  24785  metequiv2  24791  stdbdxmet  24796  nmoi  25009  reconn  25110  mulc1cncf  25188  cncfco  25190  iccpnfhmeo  25228  xrhmeo  25229  evth  25242  pi1grplem  25332  fgcfil  25554  ivthlem2  25735  ivthlem3  25736  ovolicc2lem4  25803  voliunlem1  25833  ioombl1lem4  25844  itg2gt0  26043  limcco  26175  lhop1  26296  tdeglem4  26340  plypf1  26493  coeeulem  26505  coeidlem  26518  coeid3  26521  plymul0or  26563  dvnply2  26572  plydivex  26582  plyconz  26595  vieta1lem2  26598  plyexmo  26600  aaliou3lem2  26634  ulmss  26688  ulmdvlem3  26693  iblulm  26698  sincosq2sgn  26792  sincosq3sgn  26793  sincosq4sgn  26794  logcnlem5  26938  dcubic  27138  amgm  27282  isnsqf  27426  mumullem2  27471  chtublem  27502  chtub  27503  fsumvma2  27505  vmasum  27507  dchrfi  27546  bposlem1  27575  bposlem3  27577  bposlem7  27581  lgsdir  27623  lgsquadlem2  27672  2sqlem8a  27716  2sqlem10  27719  dchrisum0flb  27801  pntpbnd1  27877  pntlemf  27896  pntlem3  27900  addonbday  28599  peano5uzs  28724  axeuclid  29475  uspgrushgr  29692  uspgrupgr  29693  usgruspgr  29695  subgrwlk  30203  usgr2pth  30284  crctcshwlkn0lem5  30337  wwlksnext  30416  wwlksnextsurj  30423  clwwlkccatlem  30514  clwlkclwwlkf  30533  clwwisshclwwslemlem  30538  lnon0  31334  normpyc  31682  ocsh  31819  ocorth  31827  ococss  31829  shsel2  31858  hsupss  31877  pjhth  31929  shlub  31950  cm2j  32156  lnfncnbd  32593  riesz1  32601  rnbra  32643  leopadd  32668  leopmuli  32669  hstles  32767  stge1i  32774  stle0i  32775  dmdbr5  32844  ssmd2  32848  superpos  32890  chcv1  32891  atoml2i  32919  chirredlem2  32927  atcvat3i  32932  mdsymlem5  32943  mdsymlem6  32944  sumdmdii  32951  sumdmdlem2  32955  isarchiofld  33694  sqsscirc2  34475  cnre2csqlem  34476  xrge0iifiso  34501  sigaclci  34698  omssubadd  34867  eulerpartlemb  34935  ballotlemimin  35073  ballotlem7  35103  fineqvac  35709  fineqvinfep  35718  vonf1wev  35812  vonf1owevOLD  35814  cusgracyclt3v  35842  cvmlift2lem12  36000  fmlasucdisj  36085  dfon2lem8  36474  segconeq  36697  ifscgr  36731  brofs2  36764  brifs2  36765  endofsegid  36772  ltnmul  36887  dissneqlem  38183  rdgellim  38219  fvineqsneq  38255  tan2h  38455  poimirlem31  38489  poimir  38491  fzmul  38595  fdc  38599  incsequz2  38603  sstotbnd2  38628  sstotbnd3  38630  totbndbnd  38643  isexid2  38709  ispridl2  38892  mpobi123f  39014  disjlem18  39755  disjdmqsss  39757  eldisjs6  39792  riotasvd  39933  lsator0sp  39978  lssatle  39992  lshpset2N  40096  lkrlspeqN  40148  omllaw2N  40221  cmtbr3N  40231  lecmtN  40233  cvlcvr1  40316  cvrval4N  40391  cvrat3  40419  3noncolr2  40426  4noncolr3  40430  3dimlem3  40438  3dimlem3OLDN  40439  3dimlem4  40441  3dimlem4OLDN  40442  llncvrlpln  40535  lplncvrlvol  40593  snatpsubN  40727  linepsubN  40729  pmapjat1  40830  pclfinclN  40927  pl42N  40960  ltrneq2  41125  cdleme7aa  41219  cdleme18d  41272  cdleme21b  41303  trlord  41546  trlcoat  41700  dochkrshp  42363  lcfl8  42479  mulgt0con1dlem  43461  irrapxlem2  43768  pell14qrdich  43814  monotoddzz  43888  pw2f1ocnv  43982  iocinico  44157  ordnexbtwnsuc  44212  tfsconcat0i  44290  naddwordnexlem4  44346  harval3  44482  sbcim2g  45465  stoweidlem62  46994  elfzelfzlble  48313  pgnbgreunbgrlem1  49133  pgnbgreunbgrlem4  49139  1arymaptf1  49676  2arymaptf1  49687  eenglngeehlnmlem2  49772  mpbiran3d  49829  opnneil  49940