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  6343  ordtr2  6426  ssimaex  6993  fliftfun  7343  isopolem  7376  isosolem  7378  f1we  7386  ordsucss  7853  f1oweALT  8008  fnse  8177  soseq  8203  brtpos  8280  issmo2  8385  onelfvnef1  8477  seqomlem1  8488  omcl  8572  oecl  8573  oawordeulem  8590  oaass  8597  omordi  8602  omord  8604  odi  8615  oen0  8623  oeordi  8624  oeordsuc  8631  nnmcl  8649  nnecl  8650  nnmordi  8668  nnmord  8669  nnmwordri  8673  nnaordex  8675  swoord1  8778  ecopovtrn  8869  f1domg  9026  pw2f1olem  9128  domtriord  9170  mapen  9188  mapxpen  9190  mapunen  9193  nndomog  9256  onomeneq  9257  inficl  9444  supmo  9471  infmo  9516  inf3lem6  9661  cantnflem1  9717  tcmin  9767  tcrank  9928  cardne  10073  cardlim  10080  cardsdomel  10082  carduni  10089  alephord  10181  cardinfima  10203  dfac5lem4  10232  infdif2  10314  cofsmo  10374  cfcoflem  10377  infpssrlem4  10411  infpssrlem5  10412  fin4en1  10414  isfin2-2  10424  enfin2i  10426  fin23lem27  10433  isf32lem12  10469  isf34lem6  10485  domtriomlem  10547  cardmin  10675  fpwwe2lem11  10753  inar1  10887  gruiun  10911  ltsonq  11081  prub  11106  reclem3pr  11161  mulcmpblnr  11183  mulgt0sr  11217  axpre-sup  11281  leltadd  11827  infm3  12303  peano5nni  12365  zextle  12799  prime  12807  uzin  13028  ublbneg  13087  zbtwnre  13100  mul2lt0bi  13255  xrre2  13327  xralrple  13362  xmulneg1  13426  supxrbnd  13485  supxrgtmnf  13486  fzrevral  13773  flge  13972  ceile  14016  modadd1  14075  modmul1  14094  modsumfzodifsn  14114  seqcl2  14190  facdiv  14458  hashss  14580  hash2exprb  14643  elfzelfzccat  14752  repswswrd  14963  cshf1  14989  cshwcsh2id  15007  rlim2lt  15693  rlim3  15694  o1lo1  15733  climshftlem  15770  o1co  15782  o1of2  15809  isercolllem2  15862  isercoll  15864  caucvgrlem2  15871  climcndslem2  16048  sqrt2irr  16446  dvds2lem  16467  dvdsle  16509  dvdsfac  16525  ltoddhalfle  16560  divalglem0  16592  ndvdsadd  16609  bitsinv1lem  16640  sadcaddlem  16656  dvdslegcd  16703  bezoutlem2  16742  bezoutlem4  16744  gcdzeq  16754  algcvga  16783  rpdvds  16864  cncongr1  16871  cncongr2  16872  prmind2  16889  isprm6  16919  rpexp  16927  eulerthlem2  16988  pclem  17045  pceulem  17052  pc2dvds  17086  fldivp1  17104  infpnlem1  17117  prmunb  17121  mrieqv2d  17842  plttr  18543  clatl  18711  idressidex0  18889  issubg4  19385  gexdvds  19828  pgpssslw  19858  sylow2alem2  19862  efgs1b  19980  efgsfo  19983  imasabl  20120  lspindpi  21440  psgnodpm  21924  psgndif  21938  obselocv  22064  pf1ind  22703  mdetunilem9  22965  matunitlindflem2  23025  fiinbas  23300  bastg  23314  tgcl  23317  opnssneib  23463  clslp  23496  tgcnp  23601  iscnp4  23611  cncls2  23621  cncls  23622  cnntr  23623  cnpresti  23636  lmss  23646  lmcnp  23652  cmpsub  23748  tgcmp  23749  dfconn2  23767  t1connperf  23784  1stcfb  23793  1stcrest  23801  kgenss  23892  llycmpkgen2  23899  txdis  23981  qtoptop2  24048  kqt0lem  24085  isr0  24086  regr1lem2  24089  cmphaushmeo  24149  fbun  24189  ssfg  24221  fgtr  24239  ufildr  24280  cnpflf  24350  fclsnei  24368  flimfnfcls  24377  fclscmp  24379  ufilcmp  24381  cnpfcf  24390  alexsublem  24393  alexsubALTlem3  24398  alexsubALTlem4  24399  ptcmplem3  24403  tgphaus  24466  tgpt1  24467  tsmsres  24493  imasdsf1olem  24722  xblss2ps  24750  xblss2  24751  blsscls2  24853  metequiv2  24859  stdbdxmet  24864  nmoi  25077  reconn  25178  mulc1cncf  25256  cncfco  25258  iccpnfhmeo  25296  xrhmeo  25297  evth  25310  pi1grplem  25400  fgcfil  25622  ivthlem2  25803  ivthlem3  25804  ovolicc2lem4  25871  voliunlem1  25901  ioombl1lem4  25912  itg2gt0  26111  limcco  26243  lhop1  26364  tdeglem4  26408  plypf1  26561  coeeulem  26573  coeidlem  26586  coeid3  26589  plymul0or  26629  dvnply2  26638  plydivex  26648  plyconz  26661  vieta1lem2  26664  plyexmo  26666  aaliou3lem2  26700  ulmss  26754  ulmdvlem3  26759  iblulm  26764  sincosq2sgn  26858  sincosq3sgn  26859  sincosq4sgn  26860  logcnlem5  27004  dcubic  27204  amgm  27348  isnsqf  27492  mumullem2  27537  chtublem  27568  chtub  27569  fsumvma2  27571  vmasum  27573  dchrfi  27612  bposlem1  27641  bposlem3  27643  bposlem7  27647  lgsdir  27689  lgsquadlem2  27738  2sqlem8a  27782  2sqlem10  27785  dchrisum0flb  27867  pntpbnd1  27943  pntlemf  27962  pntlem3  27966  addonbday  28695  peano5uzs  28820  axeuclid  29571  uspgrushgr  29788  uspgrupgr  29789  usgruspgr  29791  subgrwlk  30299  usgr2pth  30380  crctcshwlkn0lem5  30433  wwlksnext  30512  wwlksnextsurj  30519  clwwlkccatlem  30610  clwlkclwwlkf  30629  clwwisshclwwslemlem  30634  lnon0  31430  normpyc  31778  ocsh  31915  ocorth  31923  ococss  31925  shsel2  31954  hsupss  31973  pjhth  32025  shlub  32046  cm2j  32252  lnfncnbd  32689  riesz1  32697  rnbra  32739  leopadd  32764  leopmuli  32765  hstles  32863  stge1i  32870  stle0i  32871  dmdbr5  32940  ssmd2  32944  superpos  32986  chcv1  32987  atoml2i  33015  chirredlem2  33023  atcvat3i  33028  mdsymlem5  33039  mdsymlem6  33040  sumdmdii  33047  sumdmdlem2  33051  isarchiofld  33830  sqsscirc2  34611  cnre2csqlem  34612  xrge0iifiso  34637  sigaclci  34834  omssubadd  35002  eulerpartlemb  35070  ballotlemimin  35208  ballotlem7  35238  fineqvac  35884  fineqvinfep  35893  j0ltaleph  36008  vonf1wev  36036  vonf1owevOLD  36038  cusgracyclt3v  36078  cvmlift2lem12  36246  fmlasucdisj  36331  dfon2lem8  36730  segconeq  36953  ifscgr  36987  brofs2  37020  brifs2  37021  endofsegid  37028  ltnmul  37143  dissneqlem  38455  rdgellim  38491  fvineqsneq  38527  tan2h  38727  poimirlem31  38761  poimir  38763  fzmul  38867  fdc  38871  incsequz2  38875  sstotbnd2  38900  sstotbnd3  38902  totbndbnd  38915  isexid2  38981  ispridl2  39164  mpobi123f  39286  disjlem18  40027  disjdmqsss  40029  eldisjs6  40064  riotasvd  40205  lsator0sp  40250  lssatle  40264  lshpset2N  40368  lkrlspeqN  40420  omllaw2N  40493  cmtbr3N  40503  lecmtN  40505  cvlcvr1  40588  cvrval4N  40663  cvrat3  40691  3noncolr2  40698  4noncolr3  40702  3dimlem3  40710  3dimlem3OLDN  40711  3dimlem4  40713  3dimlem4OLDN  40714  llncvrlpln  40807  lplncvrlvol  40865  snatpsubN  40999  linepsubN  41001  pmapjat1  41102  pclfinclN  41199  pl42N  41232  ltrneq2  41397  cdleme7aa  41491  cdleme18d  41544  cdleme21b  41575  trlord  41818  trlcoat  41972  dochkrshp  42635  lcfl8  42751  mulgt0con1dlem  43726  irrapxlem2  44023  pell14qrdich  44069  monotoddzz  44143  pw2f1ocnv  44237  iocinico  44406  ordnexbtwnsuc  44461  tfsconcat0i  44539  naddwordnexlem4  44595  harval3  44731  sbcim2g  45712  stoweidlem62  47277  elfzelfzlble  48596  pgnbgreunbgrlem1  49416  pgnbgreunbgrlem4  49422  1arymaptf1  49959  2arymaptf1  49970  eenglngeehlnmlem2  50056  mpbiran3d  50112  opnneil  50229