Theorem sylibrd 259

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  294  sbciegft  3815  opeldmd  5905  elreldm  5933  predtrss  6321  ordtr2  6406  ssimaex  6974  fliftfun  7306  isopolem  7339  isosolem  7341  ordsucss  7803  f1oweALT  7956  fnse  8116  soseq  8142  brtpos  8217  issmo2  8346  seqomlem1  8447  omcl  8533  oecl  8534  oawordeulem  8551  oaass  8558  omordi  8563  omord  8565  odi  8576  oen0  8583  oeordi  8584  oeordsuc  8591  nnmcl  8609  nnecl  8610  nnmordi  8628  nnmord  8629  nnmwordri  8633  nnaordex  8635  swoord1  8731  ecopovtrn  8811  f1domg  8965  pw2f1olem  9073  domtriord  9120  mapen  9138  mapxpen  9140  mapunen  9143  nndomog  9213  nndomogOLD  9223  onomeneq  9225  inficl  9417  supmo  9444  infmo  9487  inf3lem6  9625  cantnflem1  9681  tcmin  9733  tcrank  9876  cardne  9957  cardlim  9964  cardsdomel  9966  carduni  9973  alephord  10067  cardinfima  10089  dfac5lem4  10118  infdif2  10202  cofsmo  10261  cfcoflem  10264  infpssrlem4  10298  infpssrlem5  10299  fin4en1  10301  isfin2-2  10311  enfin2i  10313  fin23lem27  10320  isf32lem12  10356  isf34lem6  10372  domtriomlem  10434  cardmin  10556  fpwwe2lem11  10633  inar1  10767  gruiun  10791  ltsonq  10961  prub  10986  reclem3pr  11041  mulcmpblnr  11063  mulgt0sr  11097  axpre-sup  11161  leltadd  11695  infm3  12170  peano5nni  12212  zextle  12632  prime  12640  uzin  12859  ublbneg  12914  zbtwnre  12927  mul2lt0bi  13077  xrre2  13146  xralrple  13181  xmulneg1  13245  supxrbnd  13304  supxrgtmnf  13305  fzrevral  13583  flge  13767  ceile  13811  modadd1  13870  modmul1  13886  modsumfzodifsn  13906  seqcl2  13983  facdiv  14244  hashss  14366  hash2exprb  14429  elfzelfzccat  14527  repswswrd  14731  cshf1  14757  cshwcsh2id  14776  rlim2lt  15438  rlim3  15439  o1lo1  15478  climshftlem  15515  o1co  15527  o1of2  15554  isercolllem2  15609  isercoll  15611  caucvgrlem2  15618  climcndslem2  15793  sqrt2irr  16189  dvds2lem  16209  dvdsle  16250  dvdsfac  16266  ltoddhalfle  16301  divalglem0  16333  ndvdsadd  16350  bitsinv1lem  16379  sadcaddlem  16395  dvdslegcd  16442  bezoutlem2  16479  bezoutlem4  16481  gcdzeq  16491  algcvga  16513  rpdvds  16594  cncongr1  16601  cncongr2  16602  prmind2  16619  isprm6  16648  rpexp  16656  eulerthlem2  16712  pclem  16768  pceulem  16775  pc2dvds  16809  fldivp1  16827  infpnlem1  16840  prmunb  16844  mrieqv2d  17580  plttr  18292  clatl  18458  issubg4  19020  gexdvds  19447  pgpssslw  19477  sylow2alem2  19481  efgs1b  19599  efgsfo  19602  imasabl  19739  lspindpi  20738  psgnodpm  21133  psgndif  21147  obselocv  21275  pf1ind  21866  mdetunilem9  22114  fiinbas  22447  bastg  22461  tgcl  22464  opnssneib  22611  clslp  22644  tgcnp  22749  iscnp4  22759  cncls2  22769  cncls  22770  cnntr  22771  cnpresti  22784  lmss  22794  lmcnp  22800  cmpsub  22896  tgcmp  22897  dfconn2  22915  t1connperf  22932  1stcfb  22941  1stcrest  22949  kgenss  23039  llycmpkgen2  23046  txdis  23128  qtoptop2  23195  kqt0lem  23232  isr0  23233  regr1lem2  23236  cmphaushmeo  23296  fbun  23336  ssfg  23368  fgtr  23386  ufildr  23427  cnpflf  23497  fclsnei  23515  flimfnfcls  23524  fclscmp  23526  ufilcmp  23528  cnpfcf  23537  alexsublem  23540  alexsubALTlem3  23545  alexsubALTlem4  23546  ptcmplem3  23550  tgphaus  23613  tgpt1  23614  tsmsres  23640  imasdsf1olem  23871  xblss2ps  23899  xblss2  23900  blsscls2  24005  metequiv2  24011  stdbdxmet  24016  nmoi  24237  reconn  24336  mulc1cncf  24413  cncfco  24415  iccpnfhmeo  24453  xrhmeo  24454  evth  24467  pi1grplem  24557  fgcfil  24780  ivthlem2  24961  ivthlem3  24962  ovolicc2lem4  25029  voliunlem1  25059  ioombl1lem4  25070  itg2gt0  25270  limcco  25402  lhop1  25523  tdeglem4  25569  tdeglem4OLD  25570  plypf1  25718  coeeulem  25730  coeidlem  25743  coeid3  25746  plymul0or  25786  dvnply2  25792  plydivex  25802  vieta1lem2  25816  plyexmo  25818  aaliou3lem2  25848  ulmss  25901  ulmdvlem3  25906  iblulm  25911  sincosq2sgn  26001  sincosq3sgn  26002  sincosq4sgn  26003  logcnlem5  26146  dcubic  26341  amgm  26485  isnsqf  26629  mumullem2  26674  chtublem  26704  chtub  26705  fsumvma2  26707  vmasum  26709  dchrfi  26748  bposlem1  26777  bposlem3  26779  bposlem7  26783  lgsdir  26825  lgsquadlem2  26874  2sqlem8a  26918  2sqlem10  26921  dchrisum0flb  27003  pntpbnd1  27079  pntlemf  27098  pntlem3  27102  axeuclid  28211  uspgrushgr  28425  uspgrupgr  28426  usgruspgr  28428  usgr2pth  29011  crctcshwlkn0lem5  29058  wwlksnext  29137  wwlksnextsurj  29144  clwwlkccatlem  29232  clwlkclwwlkf  29251  clwwisshclwwslemlem  29256  lnon0  30039  normpyc  30387  ocsh  30524  ocorth  30532  ococss  30534  shsel2  30563  hsupss  30582  pjhth  30634  shlub  30655  cm2j  30861  lnfncnbd  31298  riesz1  31306  rnbra  31348  leopadd  31373  leopmuli  31374  hstles  31472  stge1i  31479  stle0i  31480  dmdbr5  31549  ssmd2  31553  superpos  31595  chcv1  31596  atoml2i  31624  chirredlem2  31632  atcvat3i  31637  mdsymlem5  31648  mdsymlem6  31649  sumdmdii  31656  sumdmdlem2  31660  isarchiofld  32424  sqsscirc2  32878  cnre2csqlem  32879  xrge0iifiso  32904  sigaclci  33119  omssubadd  33288  eulerpartlemb  33356  ballotlemimin  33493  ballotlem7  33523  fineqvac  34086  subgrwlk  34112  cusgracyclt3v  34136  cvmlift2lem12  34294  fmlasucdisj  34379  dfon2lem8  34751  segconeq  34971  ifscgr  35005  brofs2  35038  brifs2  35039  endofsegid  35046  dissneqlem  36210  rdgellim  36246  fvineqsneq  36282  tan2h  36469  matunitlindflem2  36474  poimirlem31  36508  poimir  36510  fzmul  36598  fdc  36602  incsequz2  36606  sstotbnd2  36631  sstotbnd3  36633  totbndbnd  36646  isexid2  36712  ispridl2  36895  mpobi123f  37019  disjlem18  37659  disjdmqsss  37661  riotasvd  37815  lsator0sp  37860  lssatle  37874  lshpset2N  37978  lkrlspeqN  38030  omllaw2N  38103  cmtbr3N  38113  lecmtN  38115  cvlcvr1  38198  cvrval4N  38274  cvrat3  38302  3noncolr2  38309  4noncolr3  38313  3dimlem3  38321  3dimlem3OLDN  38322  3dimlem4  38324  3dimlem4OLDN  38325  llncvrlpln  38418  lplncvrlvol  38476  snatpsubN  38610  linepsubN  38612  pmapjat1  38713  pclfinclN  38810  pl42N  38843  ltrneq2  39008  cdleme7aa  39102  cdleme18d  39155  cdleme21b  39186  trlord  39429  trlcoat  39583  dochkrshp  40246  lcfl8  40362  mulgt0con1dlem  41327  irrapxlem2  41547  pell14qrdich  41593  monotoddzz  41668  pw2f1ocnv  41762  iocinico  41947  ordnexbtwnsuc  42003  tfsconcat0i  42081  naddwordnexlem4  42138  harval3  42275  sbcim2g  43285  stoweidlem62  44765  elfzelfzlble  46016  1arymaptf1  47282  2arymaptf1  47293  eenglngeehlnmlem2  47378  mpbiran3d  47436  opnneil  47496