Theorem sylbird 263

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbird.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
sylbird.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbird	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 251	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	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:  3imtr3d  296  ceqex  3566  eqreu  3646  sotr2  5479  sossfld  6021  ordintdif  6224  tz6.12i  6690  f1cofveqaeqALT  7016  soisoi  7082  riotaeqimp  7141  ov3  7314  tfindsg  7581  tfindsg2  7582  nnsuc  7603  findsg  7616  suppssr  7877  suppssrg  7878  tfrlem9  8038  oe0lem  8155  oa00  8202  omwordi  8214  om00  8218  omass  8223  oelim2  8238  oeoa  8240  oeoe  8242  nnmwordi  8278  swoso  8339  dom2lem  8581  onsdominel  8702  f1finf1o  8796  cantnfp1lem3  9190  cantnfp1  9191  cantnflem1  9199  rankr1ai  9274  rankval3b  9302  harcard  9454  infxpenlem  9487  alephnbtwn  9545  alephinit  9569  infxp  9689  cofsmo  9743  infpssALT  9787  fin23lem24  9796  fin56  9867  ttukeylem6  9988  ficard  10039  alephval2  10046  fpwwe2lem7  10111  fpwwe2  10117  gchdju1  10130  pwfseqlem3  10134  pwfseqlem4a  10135  pwfseqlem4  10136  gchpwdom  10144  tskss  10232  inar1  10249  gruss  10270  gruurn  10272  ltsonq  10443  distrlem4pr  10500  sqgt0sr  10580  map2psrpr  10584  letric  10792  renegcli  10999  addid0  11111  mulge0b  11562  nnge1  11716  0mnnnnn0  11980  nn0lt2  12098  zneo  12118  uzind2  12128  fzind  12133  nn0ind-raph  12135  uzwo  12365  nn01to3  12395  zbtwnre  12400  rpnnen1lem5  12435  ledivge1le  12515  xrletri  12601  qsqueeze  12649  difreicc  12930  elfzmlbp  13081  difelfznle  13084  elfzodifsumelfzo  13166  ssfzo12  13193  elfzonelfzo  13202  flflp1  13240  fleqceilz  13285  modsumfzodifsn  13375  addmodlteq  13377  om2uzf1oi  13384  expnngt1  13666  facdiv  13711  facwordi  13713  bcpasc  13745  hashdom  13804  hashgt23el  13849  hashdmpropge2  13907  ccatsymb  13997  swrdnnn0nd  14079  swrdnd0  14080  swrdsbslen  14087  swrdspsleq  14088  swrdlsw  14090  pfxnd0  14111  swrdswrdlem  14127  swrdccatin1  14148  pfxccatin12lem3  14155  swrdccat  14158  pfxccat3a  14161  repswswrd  14207  cshwidx0  14229  cshwcsh2id  14251  limsupbnd1  14901  lo1bdd2  14943  addcn2  15012  mulcn2  15014  o1rlimmul  15037  lo1add  15045  lo1mul  15046  rlimno1  15072  ruclem3  15648  odd2np1  15756  oddge22np1  15764  bitsfzo  15848  cncongr1  16078  2mulprm  16104  prm23ge5  16222  pcdvdsb  16275  pcaddlem  16294  infpnlem1  16316  prmunb  16320  vdwlem9  16395  vdwnnlem3  16403  ramcl  16435  prmgaplem5  16461  cshwshash  16511  setcmon  17428  setcepi  17429  setciso  17432  ghmf1  18469  sylow2alem2  18825  sylow2blem3  18829  qusabl  19068  lt6abl  19098  cyggexb  19102  gsumcom2  19178  imasring  19455  f1ghm0to0  19578  drnginvrcl  19602  drnginvrl  19604  drnginvrr  19605  subrgdvds  19632  lsmelval2  19940  quscrng  20096  xrsdsreclblem  20227  obs2ss  20509  obslbs  20510  rnasclassa  20673  mplsubrglem  20784  gsummoncoe1  21043  mp2pm2mplem4  21524  chfacfisf  21569  chfacfisfcpmat  21570  cayleyhamilton1  21607  cmpsublem  22114  cmpsub  22115  1stccnp  22177  locfincf  22246  txhaus  22362  xkohaus  22368  ufilss  22620  cfinufil  22643  fmfnfmlem1  22669  hausflim  22696  fclscf  22740  alexsubb  22761  qustgplem  22836  prdsbl  23208  metss2lem  23228  nghmcn  23462  cfil3i  23984  cmetcaulem  24003  minveclem4  24147  ovolgelb  24195  ovolunnul  24215  ovoliun  24220  ovoliunnul  24222  ovolicc2lem2  24233  iundisj2  24264  voliunlem3  24267  rolle  24704  dvlip  24707  lhop1lem  24727  lhop2  24729  dvfsumrlim  24745  deg1ge  24813  coeeulem  24935  dgrco  24986  radcnvlt1  25127  psercnlem1  25134  logcnlem2  25348  logcnlem3  25349  cxpeq  25460  angpined  25530  efrlim  25669  dmgmaddn0  25722  lgamucov  25737  basellem2  25781  ppieq0  25875  mumullem2  25879  chpeq0  25906  chteq0  25907  chtub  25910  fsumvma  25911  dchrptlem1  25962  bposlem6  25987  gausslemma2dlem0i  26062  gausslemma2dlem1a  26063  lgseisenlem2  26074  2sqlem6  26121  2sq2  26131  2sqnn0  26136  2sqreulem1  26144  2sqreunnlem1  26147  dchrisum0lem1  26214  pntrsumbnd2  26265  pntlem3  26307  colinearalg  26818  eengtrkg  26894  incistruhgr  26986  wlkv0  27554  crctcshwlkn0  27721  clwwlkccatlem  27888  clwlkclwwlklem2a4  27896  clwlkclwwlklem2  27899  clwlkclwwlkfo  27908  eucrctshift  28142  frrusgrord0  28239  frgrreg  28293  blocni  28702  ubthlem1  28767  minvecolem4  28777  shmodsi  29286  atcvati  30283  atcvat2i  30284  chirredlem4  30290  atmd2  30297  sumdmdlem  30315  addltmulALT  30343  iundisj2f  30466  iundisj2fi  30656  rngurd  31022  f1resveqaeq  32591  erdszelem9  32691  satffunlem1lem2  32895  satffunlem2lem2  32898  sotr3  33263  rdgprc  33300  soseq  33372  noextenddif  33470  nosupno  33505  nosupbnd1  33516  noinfno  33520  noinfbnd1  33531  noetasuplem4  33538  noetainflem4  33542  scutun12  33601  slerec  33610  cgrsub  33932  btwnxfr  33943  lineext  33963  linecgr  33968  btwnconn1lem4  33977  btwnconn1lem5  33978  btwnconn1lem6  33979  btwnconn1lem8  33981  btwnconn1lem11  33984  mptsnunlem  35071  finxpreclem6  35129  ltflcei  35361  poimirlem23  35396  poimirlem24  35397  poimirlem31  35404  poimirlem32  35405  ftc1anclem5  35450  heiborlem6  35570  grpokerinj  35647  dvrunz  35708  isdmn3  35828  dmncan1  35830  l1cvpat  36666  atnle  36929  cvlexch3  36944  cvlexch4N  36945  cvlatexchb1  36946  cvrat2  37041  atlelt  37050  3dimlem4a  37075  3dimlem4OLDN  37077  ps-1  37089  ps-2  37090  4atlem10  37218  4atlem11  37221  4atlem12  37224  cdleme11c  37873  cdleme21c  37939  cdlemg6d  38233  trlcoat  38335  tendoid0  38437  cdleml3N  38590  dia2dimlem7  38682  metakunt1  39683  metakunt6  39688  isdomn4  39726  fsuppind  39824  pellexlem1  40189  pellexlem6  40194  imasgim  40463  reabsifnpos  40752  reabsifnneg  40754  iunrelexpmin1  40828  iunrelexpmin2  40832  radcnvrat  41437  nzss  41440  elprneb  44033  or2expropbi  44038  tz6.12i-afv2  44227  dfatcolem  44239  f1oresf1o2  44275  zm1nn  44287  2ffzoeq  44313  sfprmdvdsmersenne  44548  lighneallem3  44552  lighneallem4  44555  requad01  44566  fppr2odd  44676  fpprwppr  44684  stgoldbwt  44721  sbgoldbaltlem1  44724  isomuspgrlem1  44772  lmod0rng  44919  0ring1eq0  44923  lidldomn1  44972  rngciso  45033  rngcisoALTV  45045  ringciso  45084  ringcisoALTV  45108  ztprmneprm  45176  lincresunit3  45315  itsclc0yqsol  45603  itschlc0xyqsol1  45605  aacllem  45827