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  5895  elreldm  5924  predtrss  6323  ordtr2  6406  ssimaex  6966  fliftfun  7310  isopolem  7343  isosolem  7345  f1we  7353  ordsucss  7812  f1oweALT  7967  fnse  8127  soseq  8153  brtpos  8229  issmo2  8334  seqomlem1  8435  omcl  8519  oecl  8520  oawordeulem  8537  oaass  8544  omordi  8549  omord  8551  odi  8562  oen0  8570  oeordi  8571  oeordsuc  8578  nnmcl  8596  nnecl  8597  nnmordi  8615  nnmord  8616  nnmwordri  8620  nnaordex  8622  swoord1  8725  ecopovtrn  8816  f1domg  8966  pw2f1olem  9067  domtriord  9109  mapen  9127  mapxpen  9129  mapunen  9132  nndomog  9195  onomeneq  9196  inficl  9383  supmo  9410  infmo  9455  inf3lem6  9600  cantnflem1  9656  tcmin  9706  tcrank  9854  cardne  9958  cardlim  9965  cardsdomel  9967  carduni  9974  alephord  10066  cardinfima  10088  dfac5lem4  10117  infdif2  10199  cofsmo  10259  cfcoflem  10262  infpssrlem4  10296  infpssrlem5  10297  fin4en1  10299  isfin2-2  10309  enfin2i  10311  fin23lem27  10318  isf32lem12  10354  isf34lem6  10370  domtriomlem  10432  cardmin  10554  fpwwe2lem11  10632  inar1  10766  gruiun  10790  ltsonq  10960  prub  10985  reclem3pr  11040  mulcmpblnr  11062  mulgt0sr  11096  axpre-sup  11160  leltadd  11704  infm3  12180  peano5nni  12242  zextle  12675  prime  12683  uzin  12904  ublbneg  12963  zbtwnre  12976  mul2lt0bi  13130  xrre2  13202  xralrple  13237  xmulneg1  13301  supxrbnd  13360  supxrgtmnf  13361  fzrevral  13647  flge  13845  ceile  13889  modadd1  13948  modmul1  13967  modsumfzodifsn  13987  seqcl2  14063  facdiv  14330  hashss  14452  hash2exprb  14515  elfzelfzccat  14624  repswswrd  14828  cshf1  14854  cshwcsh2id  14872  rlim2lt  15555  rlim3  15556  o1lo1  15595  climshftlem  15632  o1co  15644  o1of2  15671  isercolllem2  15724  isercoll  15726  caucvgrlem2  15733  climcndslem2  15911  sqrt2irr  16311  dvds2lem  16332  dvdsle  16374  dvdsfac  16390  ltoddhalfle  16425  divalglem0  16457  ndvdsadd  16474  bitsinv1lem  16505  sadcaddlem  16521  dvdslegcd  16568  bezoutlem2  16604  bezoutlem4  16606  gcdzeq  16616  algcvga  16643  rpdvds  16724  cncongr1  16731  cncongr2  16732  prmind2  16749  isprm6  16779  rpexp  16787  eulerthlem2  16847  pclem  16904  pceulem  16911  pc2dvds  16945  fldivp1  16963  infpnlem1  16976  prmunb  16980  mrieqv2d  17701  plttr  18402  clatl  18570  issubg4  19218  gexdvds  19660  pgpssslw  19690  sylow2alem2  19694  efgs1b  19812  efgsfo  19815  imasabl  19952  lspindpi  21267  psgnodpm  21749  psgndif  21763  obselocv  21889  pf1ind  22526  mdetunilem9  22788  fiinbas  23120  bastg  23134  tgcl  23137  opnssneib  23283  clslp  23316  tgcnp  23421  iscnp4  23431  cncls2  23441  cncls  23442  cnntr  23443  cnpresti  23456  lmss  23466  lmcnp  23472  cmpsub  23568  tgcmp  23569  dfconn2  23587  t1connperf  23604  1stcfb  23613  1stcrest  23621  kgenss  23711  llycmpkgen2  23718  txdis  23800  qtoptop2  23867  kqt0lem  23904  isr0  23905  regr1lem2  23908  cmphaushmeo  23968  fbun  24008  ssfg  24040  fgtr  24058  ufildr  24099  cnpflf  24169  fclsnei  24187  flimfnfcls  24196  fclscmp  24198  ufilcmp  24200  cnpfcf  24209  alexsublem  24212  alexsubALTlem3  24217  alexsubALTlem4  24218  ptcmplem3  24222  tgphaus  24285  tgpt1  24286  tsmsres  24312  imasdsf1olem  24541  xblss2ps  24569  xblss2  24570  blsscls2  24672  metequiv2  24678  stdbdxmet  24683  nmoi  24896  reconn  24997  mulc1cncf  25075  cncfco  25077  iccpnfhmeo  25115  xrhmeo  25116  evth  25129  pi1grplem  25219  fgcfil  25441  ivthlem2  25622  ivthlem3  25623  ovolicc2lem4  25690  voliunlem1  25720  ioombl1lem4  25731  itg2gt0  25930  limcco  26063  lhop1  26184  tdeglem4  26228  plypf1  26380  coeeulem  26392  coeidlem  26405  coeid3  26408  plymul0or  26450  dvnply2  26459  plydivex  26469  vieta1lem2  26483  plyexmo  26485  aaliou3lem2  26517  ulmss  26571  ulmdvlem3  26576  iblulm  26581  sincosq2sgn  26675  sincosq3sgn  26676  sincosq4sgn  26677  logcnlem5  26822  dcubic  27022  amgm  27166  isnsqf  27310  mumullem2  27355  chtublem  27386  chtub  27387  fsumvma2  27389  vmasum  27391  dchrfi  27430  bposlem1  27459  bposlem3  27461  bposlem7  27465  lgsdir  27507  lgsquadlem2  27556  2sqlem8a  27600  2sqlem10  27603  dchrisum0flb  27685  pntpbnd1  27761  pntlemf  27780  pntlem3  27784  addonbday  28483  peano5uzs  28608  axeuclid  29324  uspgrushgr  29538  uspgrupgr  29539  usgruspgr  29541  usgr2pth  30124  crctcshwlkn0lem5  30174  wwlksnext  30253  wwlksnextsurj  30260  clwwlkccatlem  30351  clwlkclwwlkf  30370  clwwisshclwwslemlem  30375  lnon0  31161  normpyc  31509  ocsh  31646  ocorth  31654  ococss  31656  shsel2  31685  hsupss  31704  pjhth  31756  shlub  31777  cm2j  31983  lnfncnbd  32420  riesz1  32428  rnbra  32470  leopadd  32495  leopmuli  32496  hstles  32594  stge1i  32601  stle0i  32602  dmdbr5  32671  ssmd2  32675  superpos  32717  chcv1  32718  atoml2i  32746  chirredlem2  32754  atcvat3i  32759  mdsymlem5  32770  mdsymlem6  32771  sumdmdii  32778  sumdmdlem2  32782  isarchiofld  33528  sqsscirc2  34308  cnre2csqlem  34309  xrge0iifiso  34334  sigaclci  34531  omssubadd  34699  eulerpartlemb  34767  ballotlemimin  34905  ballotlem7  34935  fineqvac  35537  fineqvinfep  35546  vonf1wev  35600  vonf1owevOLD  35602  subgrwlk  35632  cusgracyclt3v  35656  cvmlift2lem12  35814  fmlasucdisj  35899  dfon2lem8  36288  segconeq  36510  ifscgr  36544  brofs2  36577  brifs2  36578  endofsegid  36585  ltnmul  36716  dissneqlem  38014  rdgellim  38050  fvineqsneq  38086  tan2h  38291  matunitlindflem2  38296  poimirlem31  38330  poimir  38332  fzmul  38420  fdc  38424  incsequz2  38428  sstotbnd2  38453  sstotbnd3  38455  totbndbnd  38468  isexid2  38534  ispridl2  38717  mpobi123f  38839  disjlem18  39580  disjdmqsss  39582  eldisjs6  39617  riotasvd  39758  lsator0sp  39803  lssatle  39817  lshpset2N  39921  lkrlspeqN  39973  omllaw2N  40046  cmtbr3N  40056  lecmtN  40058  cvlcvr1  40141  cvrval4N  40216  cvrat3  40244  3noncolr2  40251  4noncolr3  40255  3dimlem3  40263  3dimlem3OLDN  40264  3dimlem4  40266  3dimlem4OLDN  40267  llncvrlpln  40360  lplncvrlvol  40418  snatpsubN  40552  linepsubN  40554  pmapjat1  40655  pclfinclN  40752  pl42N  40785  ltrneq2  40950  cdleme7aa  41044  cdleme18d  41097  cdleme21b  41128  trlord  41371  trlcoat  41525  dochkrshp  42188  lcfl8  42304  mulgt0con1dlem  43271  irrapxlem2  43578  pell14qrdich  43624  monotoddzz  43698  pw2f1ocnv  43792  iocinico  43967  ordnexbtwnsuc  44022  tfsconcat0i  44100  naddwordnexlem4  44156  harval3  44292  sbcim2g  45275  stoweidlem62  46804  elfzelfzlble  48086  pgnbgreunbgrlem1  48906  pgnbgreunbgrlem4  48912  1arymaptf1  49450  2arymaptf1  49461  eenglngeehlnmlem2  49546  mpbiran3d  49603  opnneil  49716