Theorem syl6ib 254

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ib.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	biimpi 219	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	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:  3imtr3g  298  exlimd  2218  cbvexdw  2340  ax13lem2  2375  cbvexd  2407  axc14  2462  mo3  2563  2eu3  2654  2eu6  2657  necon2bd  2948  necon2d  2955  necon4d  2956  vtoclgft  3458  spcimgft  3492  spc3egv  3508  elabgt  3570  reupick  4219  prneimg  4751  invdisj  5023  trin  5156  pwssun  5436  wefrc  5530  eqbrrdva  5723  elreldm  5789  elinxp  5874  xp11  6018  ssrnres  6021  suc11  6294  opelf  6558  dffo4  6900  onmindif2  7569  dftpos3  7964  frrlem13  8017  swoer  8399  domtriord  8770  nneneq  8807  unblem1  8901  supnub  9056  infnlb  9086  en3lplem2  9206  suc11reg  9212  inf3lem2  9222  trcl  9322  tz9.13  9372  acndom  9630  carduniima  9675  cardinfima  9676  dfac5lem5  9706  fin23lem26  9904  hsmexlem2  10006  axcc4  10018  axdc3lem2  10030  axdclem2  10099  entric  10136  alephval2  10151  cfpwsdom  10163  fpwwe2lem8  10217  ltapr  10624  supsrlem  10690  sup2  11753  nnunb  12051  nneo  12226  indstr  12477  mul2lt0bi  12657  ngtmnft  12721  qsqueeze  12756  qextlt  12758  qextle  12759  icoshft  13026  injresinj  13328  swrdccatin2  14259  rexuzre  14881  rexico  14882  summo  15246  rpnnen2lem12  15749  divalglem5  15921  ndvdssub  15933  isprm7  16228  prmdvdsncoprmbd  16246  pc2dvds  16395  infpn2  16429  vdwnnlem3  16513  mreiincl  17053  intopsn  18080  pmtrrn2  18806  psgnunilem4  18843  ablfac1eulem  19413  lbsextlem3  20151  xrsdsreclb  20364  znleval  20473  elcls3  21934  isclo2  21939  tgcn  22103  cnprest  22140  ordthaus  22235  hauscmplem  22257  comppfsc  22383  kgencn2  22408  prdstopn  22479  xkohaus  22504  qtoptop2  22550  tgqtop  22563  filufint  22771  fclsbas  22872  alexsubALTlem3  22900  alexsubALTlem4  22901  ptcmplem2  22904  cldsubg  22962  isucn2  23130  metequiv2  23362  bcthlem5  24179  vieta1  25159  aannenlem2  25176  ulmbdd  25244  angpined  25667  rlimcnp2  25803  amgm  25827  ftalem3  25911  bposlem6  26124  uhgrvd00  27576  pthdlem2lem  27808  frcond2  28304  lnon0  28833  ocnel  29333  h1dn0  29587  cnlnssadj  30115  cvnbtwn2  30322  cvnbtwn3  30323  cvnbtwn4  30324  dmdbr2  30338  dmdbr3  30340  dmdbr4  30341  superpos  30389  atcvati  30421  mdsymlem4  30441  sumdmdii  30450  cdj3lem1  30469  elicoelioo  30773  archiabl  31125  bnj1280  32667  cusgr3cyclex  32765  loop1cycl  32766  erdszelem9  32828  satfvsucsuc  32994  untangtr  33322  3orel2  33323  dfon2lem6  33434  dfon2lem7  33435  nofv  33546  sltres  33551  nogt01o  33585  nosupprefixmo  33589  noinfprefixmo  33590  noetasuplem4  33625  outsideofrflx  34115  trer  34191  elicc3  34192  nn0prpw  34198  bj-syl66ib  34421  bj-cbvexdv  34668  bj-sblem1  34712  bj-spcimdv  34767  bj-spcimdvv  34768  topdifinffinlem  35204  icorempo  35208  isbasisrelowllem1  35212  relowlpssretop  35221  difunieq  35231  fvineqsneq  35269  wl-mo3t  35417  poimirlem23  35486  poimirlem29  35492  poimirlem32  35495  poimir  35496  mblfinlem2  35501  sdclem1  35587  fdc  35589  incsequz  35592  rngosn3  35768  0rngo  35871  dmncan1  35920  bicomdd  36554  prtlem15  36575  lsatcvat  36750  lfl1  36770  hlrelat2  37103  cvrat  37122  linepsubN  37452  2llnma3r  37488  dihjatcclem4  39121  dochexmidlem1  39160  sn-dtru  39851  sn-sup2  40088  rngunsnply  40642  mptrcllem  40838  frege124d  40987  frege77  41166  frege116  41205  or3or  41249  clsk1indlem3  41271  ssralv2  41765  truniALT  41775  onfrALTlem3  41778  onfrALTlem2  41780  onfrALTlem1  41782  ax6e2ndeq  41793  stoweidlem62  43221  atbiffatnnb  44022  2reu3  44217  2reuimp  44222  gbowge7  44831  gbege6  44833  copisnmnd  44979  line2ylem  45713  line2xlem  45715  setrec1lem4  46010