Theorem sylibrd 258

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 247	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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

This theorem is referenced by:  3imtr4d  293  sbciegft  3749  opeldmd  5804  elreldm  5833  predtrss  6214  ordtr2  6295  ssimaex  6835  fliftfun  7163  isopolem  7196  isosolem  7198  ordsucss  7640  f1oweALT  7788  fnse  7945  brtpos  8022  issmo2  8151  seqomlem1  8251  omcl  8328  oecl  8329  oawordeulem  8347  oaass  8354  omordi  8359  omord  8361  odi  8372  oen0  8379  oeordi  8380  oeordsuc  8387  nnmcl  8405  nnecl  8406  nnmordi  8424  nnmord  8425  nnmwordri  8429  nnaordex  8431  swoord1  8487  ecopovtrn  8567  f1domg  8715  pw2f1olem  8816  domtriord  8859  mapen  8877  mapxpen  8879  mapunen  8882  nndomog  8904  inficl  9114  supmo  9141  infmo  9184  inf3lem6  9321  cantnflem1  9377  tcmin  9430  tcrank  9573  cardne  9654  cardlim  9661  cardsdomel  9663  carduni  9670  alephord  9762  cardinfima  9784  dfac5lem4  9813  infdif2  9897  cofsmo  9956  cfcoflem  9959  infpssrlem4  9993  infpssrlem5  9994  fin4en1  9996  isfin2-2  10006  enfin2i  10008  fin23lem27  10015  isf32lem12  10051  isf34lem6  10067  domtriomlem  10129  cardmin  10251  fpwwe2lem11  10328  inar1  10462  gruiun  10486  ltsonq  10656  prub  10681  reclem3pr  10736  mulcmpblnr  10758  mulgt0sr  10792  axpre-sup  10856  leltadd  11389  infm3  11864  peano5nni  11906  zextle  12323  prime  12331  uzin  12547  ublbneg  12602  zbtwnre  12615  mul2lt0bi  12765  xrre2  12833  xralrple  12868  xmulneg1  12932  supxrbnd  12991  supxrgtmnf  12992  fzrevral  13270  flge  13453  ceile  13497  modadd1  13556  modmul1  13572  modsumfzodifsn  13592  seqcl2  13669  facdiv  13929  hashss  14052  hash2exprb  14113  elfzelfzccat  14213  repswswrd  14425  cshf1  14451  cshwcsh2id  14469  rlim2lt  15134  rlim3  15135  o1lo1  15174  climshftlem  15211  o1co  15223  o1of2  15250  isercolllem2  15305  isercoll  15307  caucvgrlem2  15314  climcndslem2  15490  sqrt2irr  15886  dvds2lem  15906  dvdsle  15947  dvdsfac  15963  ltoddhalfle  15998  divalglem0  16030  ndvdsadd  16047  bitsinv1lem  16076  sadcaddlem  16092  dvdslegcd  16139  bezoutlem2  16176  bezoutlem4  16178  gcdzeq  16190  algcvga  16212  rpdvds  16293  cncongr1  16300  cncongr2  16301  prmind2  16318  isprm6  16347  rpexp  16355  eulerthlem2  16411  pclem  16467  pceulem  16474  pc2dvds  16508  fldivp1  16526  infpnlem1  16539  prmunb  16543  mrieqv2d  17265  plttr  17975  clatl  18141  issubg4  18689  gexdvds  19104  pgpssslw  19134  sylow2alem2  19138  efgs1b  19257  efgsfo  19260  lspindpi  20309  psgnodpm  20705  psgndif  20719  obselocv  20845  pf1ind  21431  mdetunilem9  21677  fiinbas  22010  bastg  22024  tgcl  22027  opnssneib  22174  clslp  22207  tgcnp  22312  iscnp4  22322  cncls2  22332  cncls  22333  cnntr  22334  cnpresti  22347  lmss  22357  lmcnp  22363  cmpsub  22459  tgcmp  22460  dfconn2  22478  t1connperf  22495  1stcfb  22504  1stcrest  22512  kgenss  22602  llycmpkgen2  22609  txdis  22691  qtoptop2  22758  kqt0lem  22795  isr0  22796  regr1lem2  22799  cmphaushmeo  22859  fbun  22899  ssfg  22931  fgtr  22949  ufildr  22990  cnpflf  23060  fclsnei  23078  flimfnfcls  23087  fclscmp  23089  ufilcmp  23091  cnpfcf  23100  alexsublem  23103  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem3  23113  tgphaus  23176  tgpt1  23177  tsmsres  23203  imasdsf1olem  23434  xblss2ps  23462  xblss2  23463  blsscls2  23566  metequiv2  23572  stdbdxmet  23577  nmoi  23798  reconn  23897  mulc1cncf  23974  cncfco  23976  iccpnfhmeo  24014  xrhmeo  24015  evth  24028  pi1grplem  24118  fgcfil  24340  ivthlem2  24521  ivthlem3  24522  ovolicc2lem4  24589  voliunlem1  24619  ioombl1lem4  24630  itg2gt0  24830  limcco  24962  lhop1  25083  tdeglem4  25129  tdeglem4OLD  25130  plypf1  25278  coeeulem  25290  coeidlem  25303  coeid3  25306  plymul0or  25346  dvnply2  25352  plydivex  25362  vieta1lem2  25376  plyexmo  25378  aaliou3lem2  25408  ulmss  25461  ulmdvlem3  25466  iblulm  25471  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  logcnlem5  25706  dcubic  25901  amgm  26045  isnsqf  26189  mumullem2  26234  chtublem  26264  chtub  26265  fsumvma2  26267  vmasum  26269  dchrfi  26308  bposlem1  26337  bposlem3  26339  bposlem7  26343  lgsdir  26385  lgsquadlem2  26434  2sqlem8a  26478  2sqlem10  26481  dchrisum0flb  26563  pntpbnd1  26639  pntlemf  26658  pntlem3  26662  axeuclid  27234  uspgrushgr  27448  uspgrupgr  27449  usgruspgr  27451  usgr2pth  28033  crctcshwlkn0lem5  28080  wwlksnext  28159  wwlksnextsurj  28166  clwwlkccatlem  28254  clwlkclwwlkf  28273  clwwisshclwwslemlem  28278  lnon0  29061  normpyc  29409  ocsh  29546  ocorth  29554  ococss  29556  shsel2  29585  hsupss  29604  pjhth  29656  shlub  29677  cm2j  29883  lnfncnbd  30320  riesz1  30328  rnbra  30370  leopadd  30395  leopmuli  30396  hstles  30494  stge1i  30501  stle0i  30502  dmdbr5  30571  ssmd2  30575  superpos  30617  chcv1  30618  atoml2i  30646  chirredlem2  30654  atcvat3i  30659  mdsymlem5  30670  mdsymlem6  30671  sumdmdii  30678  sumdmdlem2  30682  isarchiofld  31418  sqsscirc2  31761  cnre2csqlem  31762  xrge0iifiso  31787  sigaclci  32000  omssubadd  32167  eulerpartlemb  32235  ballotlemimin  32372  ballotlem7  32402  fineqvac  32966  subgrwlk  32994  cusgracyclt3v  33018  cvmlift2lem12  33176  fmlasucdisj  33261  dfon2lem8  33672  soseq  33730  segconeq  34239  ifscgr  34273  brofs2  34306  brifs2  34307  endofsegid  34314  dissneqlem  35438  rdgellim  35474  fvineqsneq  35510  tan2h  35696  matunitlindflem2  35701  poimirlem31  35735  poimir  35737  fzmul  35826  fdc  35830  incsequz2  35834  sstotbnd2  35859  sstotbnd3  35861  totbndbnd  35874  isexid2  35940  ispridl2  36123  mpobi123f  36247  riotasvd  36897  lsator0sp  36942  lssatle  36956  lshpset2N  37060  lkrlspeqN  37112  omllaw2N  37185  cmtbr3N  37195  lecmtN  37197  cvlcvr1  37280  cvrval4N  37355  cvrat3  37383  3noncolr2  37390  4noncolr3  37394  3dimlem3  37402  3dimlem3OLDN  37403  3dimlem4  37405  3dimlem4OLDN  37406  llncvrlpln  37499  lplncvrlvol  37557  snatpsubN  37691  linepsubN  37693  pmapjat1  37794  pclfinclN  37891  pl42N  37924  ltrneq2  38089  cdleme7aa  38183  cdleme18d  38236  cdleme21b  38267  trlord  38510  trlcoat  38664  dochkrshp  39327  lcfl8  39443  mulgt0con1dlem  40348  irrapxlem2  40561  pell14qrdich  40607  monotoddzz  40681  pw2f1ocnv  40775  iocinico  40959  harval3  41041  sbcim2g  42047  stoweidlem62  43493  elfzelfzlble  44701  1arymaptf1  45876  2arymaptf1  45887  eenglngeehlnmlem2  45972  mpbiran3d  46030  opnneil  46091