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 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:  3imtr3d  296  ceqex  3609  eqreu  3690  sotr2  5601  sotr3  5608  sossfld  6183  ordintdif  6413  tz6.12i  6908  f1cofveqaeqALT  7258  f1resveqaeq  7273  soisoi  7332  riotaeqimp  7399  ov3  7579  tfindsg  7860  tfindsg2  7861  nnsuc  7883  findsg  7897  soseq  8160  suppssr  8196  suppssrg  8197  tfrlem9  8377  oe0lem  8503  oa00  8549  omwordi  8561  om00  8565  omass  8570  oelim2  8586  oeoa  8588  oeoe  8590  nnmwordi  8626  swoso  8734  dom2lem  9001  onsdominel  9127  f1finf1o  9246  fiint  9299  cantnfp1lem3  9662  cantnfp1  9663  cantnflem1  9671  ttrclselem2  9708  rankr1ai  9783  rankval3b  9811  harcard  9986  infxpenlem  10019  alephnbtwn  10077  alephinit  10101  infxp  10219  cofsmo  10274  infpssALT  10318  fin23lem24  10327  fin56  10398  ttukeylem6  10519  ficard  10576  alephval2  10584  fpwwe2lem7  10649  fpwwe2  10655  gchdju1  10668  pwfseqlem3  10672  pwfseqlem4a  10673  pwfseqlem4  10674  gchpwdom  10682  tskss  10770  inar1  10787  gruss  10808  gruurn  10810  ltsonq  10981  distrlem4pr  11038  sqgt0sr  11118  map2psrpr  11122  letric  11337  renegcli  11546  addid0  11660  mulge0b  12112  nnge1  12291  0mnnnnn0  12563  nn0lt2  12687  zneo  12707  uzind2  12717  fzind  12722  nn0ind-raph  12724  uzwo  12963  nn01to3  12993  zbtwnre  12998  rpnnen1lem5  13033  ledivge1le  13117  xrletri  13206  qsqueeze  13255  difreicc  13539  elfzmlbp  13696  difelfznle  13699  elfzodifsumelfzo  13789  ssfzo12  13817  elfzonelfzo  13827  flflp1  13870  fleqceilz  13917  modsumfzodifsn  14010  addmodlteq  14012  om2uzf1oi  14019  expnngt1  14307  facdiv  14353  facwordi  14355  bcpasc  14387  hashdom  14445  hashgt23el  14491  hashdmpropge2  14550  ccatsymb  14650  swrdnnn0nd  14728  swrdnd0  14729  swrdsbslen  14736  swrdspsleq  14737  swrdlsw  14739  pfxnd0  14760  swrdswrdlem  14775  swrdccatin1  14796  pfxccatin12lem3  14803  swrdccat  14806  pfxccat3a  14809  repswswrd  14857  cshwidx0  14879  cshwcsh2id  14901  limsupbnd1  15571  lo1bdd2  15613  addcn2  15683  mulcn2  15685  o1rlimmul  15708  lo1add  15716  lo1mul  15717  rlimno1  15743  ruclem3  16325  odd2np1  16435  oddge22np1  16443  bitsfzo  16529  cncongr1  16761  2mulprm  16787  prm23ge5  16911  pcdvdsb  16965  pcaddlem  16984  infpnlem1  17006  prmunb  17010  vdwlem9  17085  vdwnnlem3  17093  ramcl  17125  prmgaplem5  17151  cshwshash  17200  setcmon  18180  setcepi  18181  setciso  18184  xpsmnd0  18889  f1ghm0to0  19376  ghmf1  19377  sylow2alem2  19749  sylow2blem3  19753  qusabl  19996  lt6abl  20026  cyggexb  20030  gsumcom2  20106  ringurd  20328  imasring  20475  xpsring1d  20478  0ring1eq0  20699  subrgdvds  20752  rngciso  20804  ringciso  20838  isdomn4  20881  drnginvrcl  20924  drnginvrl  20927  drnginvrr  20928  lsmelval2  21273  quscrng  21490  xrsdsreclblem  21630  obs2ss  21946  obslbs  21947  rnasclassa  22114  mplsubrglem  22222  psdmul  22398  gsummoncoe1  22537  mp2pm2mplem4  23038  chfacfisf  23083  chfacfisfcpmat  23084  cayleyhamilton1  23121  cmpsublem  23628  cmpsub  23629  1stccnp  23692  locfincf  23761  txhaus  23877  xkohaus  23883  ufilss  24135  cfinufil  24158  fmfnfmlem1  24184  hausflim  24211  fclscf  24255  alexsubb  24276  qustgplem  24351  prdsbl  24721  metss2lem  24741  nghmcn  24975  cfil3i  25501  cmetcaulem  25520  minveclem4  25664  ovolgelb  25712  ovolunnul  25732  ovoliun  25737  ovoliunnul  25739  ovolicc2lem2  25750  iundisj2  25781  voliunlem3  25784  rolle  26222  dvlip  26225  lhop1lem  26245  lhop2  26247  dvfsumrlim  26263  deg1ge  26328  coeeulem  26454  dgrco  26505  radcnvlt1  26654  psercnlem1  26661  logcnlem2  26881  logcnlem3  26882  cxpeq  26995  angpined  27068  efrlim  27207  dmgmaddn0  27260  lgamucov  27275  basellem2  27319  ppieq0  27413  mumullem2  27417  chpeq0  27445  chteq0  27446  chtub  27449  fsumvma  27450  dchrptlem1  27501  bposlem6  27526  gausslemma2dlem0i  27601  gausslemma2dlem1a  27602  lgseisenlem2  27613  2sqlem6  27660  2sq2  27670  2sqnn0  27675  2sqreulem1  27683  2sqreunnlem1  27686  dchrisum0lem1  27753  pntrsumbnd2  27804  pntlem3  27846  noextenddif  27905  nosupno  27940  nosupbnd1  27951  noinfno  27955  noinfbnd1  27966  noetasuplem4  27973  noetainflem4  27977  cutsun12  28056  lesrec  28065  cutlt  28198  leadds2im  28254  oniso  28537  n0fincut  28621  bdayfinbndlem1  28733  z12bdaylem1  28736  colinearalg  29368  eengtrkg  29444  incistruhgr  29537  wlkv0  30110  crctcshwlkn0  30290  clwwlkccatlem  30460  clwlkclwwlklem2a4  30468  clwlkclwwlklem2  30471  clwlkclwwlkfo  30480  eucrctshift  30724  frrusgrord0  30821  frgrreg  30875  blocni  31287  ubthlem1  31352  minvecolem4  31362  shmodsi  31871  atcvati  32868  atcvat2i  32869  chirredlem4  32875  atmd2  32882  sumdmdlem  32900  addltmulALT  32928  iundisj2f  33065  iundisj2fi  33270  erdszelem9  35780  satffunlem1lem2  35984  satffunlem2lem2  35987  rdgprc  36373  cgrsub  36627  btwnxfr  36638  lineext  36658  linecgr  36663  btwnconn1lem4  36672  btwnconn1lem5  36673  btwnconn1lem6  36674  btwnconn1lem8  36676  btwnconn1lem11  36679  mh-inf3f1  37162  mptsnunlem  38094  finxpreclem6  38152  ltflcei  38364  poimirlem23  38394  poimirlem24  38395  poimirlem31  38402  poimirlem32  38403  ftc1anclem5  38448  heiborlem6  38568  grpokerinj  38645  dvrunz  38706  isdmn3  38826  dmncan1  38828  membpartlem19  39664  l1cvpat  39929  atnle  40192  cvlexch3  40207  cvlexch4N  40208  cvlatexchb1  40209  cvrat2  40304  atlelt  40313  3dimlem4a  40338  3dimlem4OLDN  40340  ps-1  40352  ps-2  40353  4atlem10  40481  4atlem11  40484  4atlem12  40487  cdleme11c  41136  cdleme21c  41202  cdlemg6d  41496  trlcoat  41598  tendoid0  41700  cdleml3N  41853  dia2dimlem7  41945  aks6d1c6lem3  43040  expeq1d  43201  fsuppind  43438  pellexlem1  43672  pellexlem6  43677  imasgim  43943  onsupmaxb  44082  safesnsupfidom1o  44259  reabsifnpos  44475  reabsifnneg  44477  iunrelexpmin1  44550  iunrelexpmin2  44554  radcnvrat  45140  nzss  45143  pwclaxpow  45809  ormkglobd  47707  elprneb  47919  or2expropbi  47924  tz6.12i-afv2  48133  dfatcolem  48145  f1oresf1o2  48181  zm1nn  48192  2ffzoeq  48218  modmkpkne  48257  sfprmdvdsmersenne  48508  lighneallem3  48512  lighneallem4  48515  requad01  48539  fppr2odd  48649  fpprwppr  48657  stgoldbwt  48694  sbgoldbaltlem1  48697  isuspgrimlem  48813  upgrimpthslem2  48826  isubgr3stgrlem4  48887  isubgr3stgrlem7  48890  gpg5nbgrvtx03starlem1  48986  gpg5nbgrvtx03starlem3  48988  gpg5nbgrvtx13starlem1  48989  gpg5nbgrvtx13starlem3  48991  lmod0rng  49146  lidldomn1  49148  rngcisoALTV  49194  ringcisoALTV  49228  isidom3  49262  idomcanl  49264  ztprmneprm  49279  lincresunit3  49413  itsclc0yqsol  49696  itschlc0xyqsol1  49698  aacllem  50774