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  5894  elreldm  5923  predtrss  6324  ordtr2  6407  ssimaex  6967  fliftfun  7316  isopolem  7349  isosolem  7351  f1we  7359  ordsucss  7817  f1oweALT  7972  fnse  8134  soseq  8160  brtpos  8236  issmo2  8341  seqomlem1  8442  omcl  8526  oecl  8527  oawordeulem  8544  oaass  8551  omordi  8556  omord  8558  odi  8569  oen0  8577  oeordi  8578  oeordsuc  8585  nnmcl  8603  nnecl  8604  nnmordi  8622  nnmord  8623  nnmwordri  8627  nnaordex  8629  swoord1  8732  ecopovtrn  8823  f1domg  8980  pw2f1olem  9082  domtriord  9124  mapen  9142  mapxpen  9144  mapunen  9147  nndomog  9210  onomeneq  9211  inficl  9398  supmo  9425  infmo  9470  inf3lem6  9615  cantnflem1  9671  tcmin  9721  tcrank  9869  cardne  9973  cardlim  9980  cardsdomel  9982  carduni  9989  alephord  10081  cardinfima  10103  dfac5lem4  10132  infdif2  10214  cofsmo  10274  cfcoflem  10277  infpssrlem4  10311  infpssrlem5  10312  fin4en1  10314  isfin2-2  10324  enfin2i  10326  fin23lem27  10333  isf32lem12  10369  isf34lem6  10385  domtriomlem  10447  cardmin  10575  fpwwe2lem11  10653  inar1  10787  gruiun  10811  ltsonq  10981  prub  11006  reclem3pr  11061  mulcmpblnr  11083  mulgt0sr  11117  axpre-sup  11181  leltadd  11725  infm3  12201  peano5nni  12263  zextle  12697  prime  12705  uzin  12926  ublbneg  12985  zbtwnre  12998  mul2lt0bi  13152  xrre2  13224  xralrple  13259  xmulneg1  13323  supxrbnd  13382  supxrgtmnf  13383  fzrevral  13669  flge  13868  ceile  13912  modadd1  13971  modmul1  13990  modsumfzodifsn  14010  seqcl2  14086  facdiv  14353  hashss  14475  hash2exprb  14538  elfzelfzccat  14647  repswswrd  14857  cshf1  14883  cshwcsh2id  14901  rlim2lt  15586  rlim3  15587  o1lo1  15626  climshftlem  15663  o1co  15675  o1of2  15702  isercolllem2  15755  isercoll  15757  caucvgrlem2  15764  climcndslem2  15941  sqrt2irr  16341  dvds2lem  16362  dvdsle  16404  dvdsfac  16420  ltoddhalfle  16455  divalglem0  16487  ndvdsadd  16504  bitsinv1lem  16535  sadcaddlem  16551  dvdslegcd  16598  bezoutlem2  16634  bezoutlem4  16636  gcdzeq  16646  algcvga  16673  rpdvds  16754  cncongr1  16761  cncongr2  16762  prmind2  16779  isprm6  16809  rpexp  16817  eulerthlem2  16877  pclem  16934  pceulem  16941  pc2dvds  16975  fldivp1  16993  infpnlem1  17006  prmunb  17010  mrieqv2d  17731  plttr  18432  clatl  18600  idressidex0  18777  issubg4  19273  gexdvds  19715  pgpssslw  19745  sylow2alem2  19749  efgs1b  19867  efgsfo  19870  imasabl  20007  lspindpi  21323  psgnodpm  21805  psgndif  21819  obselocv  21945  pf1ind  22584  mdetunilem9  22846  matunitlindflem2  22906  fiinbas  23181  bastg  23195  tgcl  23198  opnssneib  23344  clslp  23377  tgcnp  23482  iscnp4  23492  cncls2  23502  cncls  23503  cnntr  23504  cnpresti  23517  lmss  23527  lmcnp  23533  cmpsub  23629  tgcmp  23630  dfconn2  23648  t1connperf  23665  1stcfb  23674  1stcrest  23682  kgenss  23773  llycmpkgen2  23780  txdis  23862  qtoptop2  23929  kqt0lem  23966  isr0  23967  regr1lem2  23970  cmphaushmeo  24030  fbun  24070  ssfg  24102  fgtr  24120  ufildr  24161  cnpflf  24231  fclsnei  24249  flimfnfcls  24258  fclscmp  24260  ufilcmp  24262  cnpfcf  24271  alexsublem  24274  alexsubALTlem3  24279  alexsubALTlem4  24280  ptcmplem3  24284  tgphaus  24347  tgpt1  24348  tsmsres  24374  imasdsf1olem  24603  xblss2ps  24631  xblss2  24632  blsscls2  24734  metequiv2  24740  stdbdxmet  24745  nmoi  24958  reconn  25059  mulc1cncf  25137  cncfco  25139  iccpnfhmeo  25177  xrhmeo  25178  evth  25191  pi1grplem  25281  fgcfil  25503  ivthlem2  25684  ivthlem3  25685  ovolicc2lem4  25752  voliunlem1  25782  ioombl1lem4  25793  itg2gt0  25992  limcco  26125  lhop1  26246  tdeglem4  26290  plypf1  26442  coeeulem  26454  coeidlem  26467  coeid3  26470  plymul0or  26512  dvnply2  26521  plydivex  26531  vieta1lem2  26545  plyexmo  26547  aaliou3lem2  26579  ulmss  26633  ulmdvlem3  26638  iblulm  26643  sincosq2sgn  26737  sincosq3sgn  26738  sincosq4sgn  26739  logcnlem5  26884  dcubic  27084  amgm  27228  isnsqf  27372  mumullem2  27417  chtublem  27448  chtub  27449  fsumvma2  27451  vmasum  27453  dchrfi  27492  bposlem1  27521  bposlem3  27523  bposlem7  27527  lgsdir  27569  lgsquadlem2  27618  2sqlem8a  27662  2sqlem10  27665  dchrisum0flb  27747  pntpbnd1  27823  pntlemf  27842  pntlem3  27846  addonbday  28545  peano5uzs  28670  axeuclid  29421  uspgrushgr  29638  uspgrupgr  29639  usgruspgr  29641  subgrwlk  30149  usgr2pth  30230  crctcshwlkn0lem5  30283  wwlksnext  30362  wwlksnextsurj  30369  clwwlkccatlem  30460  clwlkclwwlkf  30479  clwwisshclwwslemlem  30484  lnon0  31280  normpyc  31628  ocsh  31765  ocorth  31773  ococss  31775  shsel2  31804  hsupss  31823  pjhth  31875  shlub  31896  cm2j  32102  lnfncnbd  32539  riesz1  32547  rnbra  32589  leopadd  32614  leopmuli  32615  hstles  32713  stge1i  32720  stle0i  32721  dmdbr5  32790  ssmd2  32794  superpos  32836  chcv1  32837  atoml2i  32865  chirredlem2  32873  atcvat3i  32878  mdsymlem5  32889  mdsymlem6  32890  sumdmdii  32897  sumdmdlem2  32901  isarchiofld  33641  sqsscirc2  34421  cnre2csqlem  34422  xrge0iifiso  34447  sigaclci  34644  omssubadd  34813  eulerpartlemb  34881  ballotlemimin  35019  ballotlem7  35049  fineqvac  35644  fineqvinfep  35653  vonf1wev  35707  vonf1owevOLD  35709  cusgracyclt3v  35737  cvmlift2lem12  35895  fmlasucdisj  35980  dfon2lem8  36369  segconeq  36592  ifscgr  36626  brofs2  36659  brifs2  36660  endofsegid  36667  ltnmul  36798  dissneqlem  38096  rdgellim  38132  fvineqsneq  38168  tan2h  38368  poimirlem31  38402  poimir  38404  fzmul  38493  fdc  38497  incsequz2  38501  sstotbnd2  38526  sstotbnd3  38528  totbndbnd  38541  isexid2  38607  ispridl2  38790  mpobi123f  38912  disjlem18  39653  disjdmqsss  39655  eldisjs6  39690  riotasvd  39831  lsator0sp  39876  lssatle  39890  lshpset2N  39994  lkrlspeqN  40046  omllaw2N  40119  cmtbr3N  40129  lecmtN  40131  cvlcvr1  40214  cvrval4N  40289  cvrat3  40317  3noncolr2  40324  4noncolr3  40328  3dimlem3  40336  3dimlem3OLDN  40337  3dimlem4  40339  3dimlem4OLDN  40340  llncvrlpln  40433  lplncvrlvol  40491  snatpsubN  40625  linepsubN  40627  pmapjat1  40728  pclfinclN  40825  pl42N  40858  ltrneq2  41023  cdleme7aa  41117  cdleme18d  41170  cdleme21b  41201  trlord  41444  trlcoat  41598  dochkrshp  42261  lcfl8  42377  mulgt0con1dlem  43359  irrapxlem2  43666  pell14qrdich  43712  monotoddzz  43786  pw2f1ocnv  43880  iocinico  44055  ordnexbtwnsuc  44110  tfsconcat0i  44188  naddwordnexlem4  44244  harval3  44380  sbcim2g  45363  stoweidlem62  46892  elfzelfzlble  48211  pgnbgreunbgrlem1  49031  pgnbgreunbgrlem4  49037  1arymaptf1  49574  2arymaptf1  49585  eenglngeehlnmlem2  49670  mpbiran3d  49727  opnneil  49838