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  5896  elreldm  5925  predtrss  6323  ordtr2  6406  ssimaex  6966  fliftfun  7310  isopolem  7343  isosolem  7345  ordsucss  7813  f1oweALT  7968  fnse  8128  soseq  8154  brtpos  8230  issmo2  8335  seqomlem1  8436  omcl  8520  oecl  8521  oawordeulem  8538  oaass  8545  omordi  8550  omord  8552  odi  8563  oen0  8571  oeordi  8572  oeordsuc  8579  nnmcl  8597  nnecl  8598  nnmordi  8616  nnmord  8617  nnmwordri  8621  nnaordex  8623  swoord1  8726  ecopovtrn  8817  f1domg  8967  pw2f1olem  9068  domtriord  9110  mapen  9128  mapxpen  9130  mapunen  9133  nndomog  9196  onomeneq  9197  inficl  9384  supmo  9411  infmo  9456  inf3lem6  9601  cantnflem1  9657  tcmin  9707  tcrank  9855  cardne  9950  cardlim  9957  cardsdomel  9959  carduni  9966  alephord  10058  cardinfima  10080  dfac5lem4  10109  infdif2  10191  cofsmo  10252  cfcoflem  10255  infpssrlem4  10289  infpssrlem5  10290  fin4en1  10292  isfin2-2  10302  enfin2i  10304  fin23lem27  10311  isf32lem12  10347  isf34lem6  10363  domtriomlem  10425  cardmin  10547  fpwwe2lem11  10625  inar1  10759  gruiun  10783  ltsonq  10953  prub  10978  reclem3pr  11033  mulcmpblnr  11055  mulgt0sr  11089  axpre-sup  11153  leltadd  11697  infm3  12173  peano5nni  12235  zextle  12668  prime  12676  uzin  12897  ublbneg  12956  zbtwnre  12969  mul2lt0bi  13123  xrre2  13195  xralrple  13230  xmulneg1  13294  supxrbnd  13353  supxrgtmnf  13354  fzrevral  13640  flge  13838  ceile  13882  modadd1  13941  modmul1  13960  modsumfzodifsn  13980  seqcl2  14056  facdiv  14323  hashss  14445  hash2exprb  14508  elfzelfzccat  14617  repswswrd  14821  cshf1  14847  cshwcsh2id  14865  rlim2lt  15548  rlim3  15549  o1lo1  15588  climshftlem  15625  o1co  15637  o1of2  15664  isercolllem2  15717  isercoll  15719  caucvgrlem2  15726  climcndslem2  15904  sqrt2irr  16304  dvds2lem  16325  dvdsle  16367  dvdsfac  16383  ltoddhalfle  16418  divalglem0  16450  ndvdsadd  16467  bitsinv1lem  16498  sadcaddlem  16514  dvdslegcd  16561  bezoutlem2  16597  bezoutlem4  16599  gcdzeq  16609  algcvga  16636  rpdvds  16717  cncongr1  16724  cncongr2  16725  prmind2  16742  isprm6  16772  rpexp  16780  eulerthlem2  16840  pclem  16897  pceulem  16904  pc2dvds  16938  fldivp1  16956  infpnlem1  16969  prmunb  16973  mrieqv2d  17694  plttr  18395  clatl  18563  issubg4  19211  gexdvds  19653  pgpssslw  19683  sylow2alem2  19687  efgs1b  19805  efgsfo  19808  imasabl  19945  lspindpi  21235  psgnodpm  21717  psgndif  21731  obselocv  21857  pf1ind  22494  mdetunilem9  22756  fiinbas  23088  bastg  23102  tgcl  23105  opnssneib  23251  clslp  23284  tgcnp  23389  iscnp4  23399  cncls2  23409  cncls  23410  cnntr  23411  cnpresti  23424  lmss  23434  lmcnp  23440  cmpsub  23536  tgcmp  23537  dfconn2  23555  t1connperf  23572  1stcfb  23581  1stcrest  23589  kgenss  23679  llycmpkgen2  23686  txdis  23768  qtoptop2  23835  kqt0lem  23872  isr0  23873  regr1lem2  23876  cmphaushmeo  23936  fbun  23976  ssfg  24008  fgtr  24026  ufildr  24067  cnpflf  24137  fclsnei  24155  flimfnfcls  24164  fclscmp  24166  ufilcmp  24168  cnpfcf  24177  alexsublem  24180  alexsubALTlem3  24185  alexsubALTlem4  24186  ptcmplem3  24190  tgphaus  24253  tgpt1  24254  tsmsres  24280  imasdsf1olem  24509  xblss2ps  24537  xblss2  24538  blsscls2  24640  metequiv2  24646  stdbdxmet  24651  nmoi  24864  reconn  24965  mulc1cncf  25043  cncfco  25045  iccpnfhmeo  25083  xrhmeo  25084  evth  25097  pi1grplem  25187  fgcfil  25409  ivthlem2  25590  ivthlem3  25591  ovolicc2lem4  25658  voliunlem1  25688  ioombl1lem4  25699  itg2gt0  25898  limcco  26031  lhop1  26152  tdeglem4  26196  plypf1  26348  coeeulem  26360  coeidlem  26373  coeid3  26376  plymul0or  26418  dvnply2  26427  plydivex  26437  vieta1lem2  26451  plyexmo  26453  aaliou3lem2  26483  ulmss  26536  ulmdvlem3  26541  iblulm  26546  sincosq2sgn  26640  sincosq3sgn  26641  sincosq4sgn  26642  logcnlem5  26787  dcubic  26987  amgm  27131  isnsqf  27275  mumullem2  27320  chtublem  27351  chtub  27352  fsumvma2  27354  vmasum  27356  dchrfi  27395  bposlem1  27424  bposlem3  27426  bposlem7  27430  lgsdir  27472  lgsquadlem2  27521  2sqlem8a  27565  2sqlem10  27568  dchrisum0flb  27650  pntpbnd1  27726  pntlemf  27745  pntlem3  27749  addonbday  28448  peano5uzs  28573  axeuclid  29279  uspgrushgr  29493  uspgrupgr  29494  usgruspgr  29496  usgr2pth  30079  crctcshwlkn0lem5  30129  wwlksnext  30208  wwlksnextsurj  30215  clwwlkccatlem  30306  clwlkclwwlkf  30325  clwwisshclwwslemlem  30330  lnon0  31116  normpyc  31464  ocsh  31601  ocorth  31609  ococss  31611  shsel2  31640  hsupss  31659  pjhth  31711  shlub  31732  cm2j  31938  lnfncnbd  32375  riesz1  32383  rnbra  32425  leopadd  32450  leopmuli  32451  hstles  32549  stge1i  32556  stle0i  32557  dmdbr5  32626  ssmd2  32630  superpos  32672  chcv1  32673  atoml2i  32701  chirredlem2  32709  atcvat3i  32714  mdsymlem5  32725  mdsymlem6  32726  sumdmdii  32733  sumdmdlem2  32737  isarchiofld  33485  sqsscirc2  34265  cnre2csqlem  34266  xrge0iifiso  34291  sigaclci  34488  omssubadd  34656  eulerpartlemb  34724  ballotlemimin  34862  ballotlem7  34892  fineqvac  35495  fineqvinfep  35504  vonf1wev  35558  vonf1owevOLD  35560  subgrwlk  35590  cusgracyclt3v  35614  cvmlift2lem12  35772  fmlasucdisj  35857  dfon2lem8  36246  segconeq  36468  ifscgr  36502  brofs2  36535  brifs2  36536  endofsegid  36543  ltnmul  36659  dissneqlem  37952  rdgellim  37988  fvineqsneq  38024  tan2h  38229  matunitlindflem2  38234  poimirlem31  38268  poimir  38270  fzmul  38358  fdc  38362  incsequz2  38366  sstotbnd2  38391  sstotbnd3  38393  totbndbnd  38406  isexid2  38472  ispridl2  38655  mpobi123f  38779  disjlem18  39520  disjdmqsss  39522  eldisjs6  39557  riotasvd  39698  lsator0sp  39743  lssatle  39757  lshpset2N  39861  lkrlspeqN  39913  omllaw2N  39986  cmtbr3N  39996  lecmtN  39998  cvlcvr1  40081  cvrval4N  40156  cvrat3  40184  3noncolr2  40191  4noncolr3  40195  3dimlem3  40203  3dimlem3OLDN  40204  3dimlem4  40206  3dimlem4OLDN  40207  llncvrlpln  40300  lplncvrlvol  40358  snatpsubN  40492  linepsubN  40494  pmapjat1  40595  pclfinclN  40692  pl42N  40725  ltrneq2  40890  cdleme7aa  40984  cdleme18d  41037  cdleme21b  41068  trlord  41311  trlcoat  41465  dochkrshp  42128  lcfl8  42244  mulgt0con1dlem  43211  irrapxlem2  43520  pell14qrdich  43566  monotoddzz  43640  pw2f1ocnv  43734  iocinico  43909  ordnexbtwnsuc  43964  tfsconcat0i  44042  naddwordnexlem4  44098  harval3  44234  sbcim2g  45217  stoweidlem62  46746  elfzelfzlble  48025  pgnbgreunbgrlem1  48845  pgnbgreunbgrlem4  48851  1arymaptf1  49389  2arymaptf1  49400  eenglngeehlnmlem2  49485  mpbiran3d  49542  opnneil  49655