Theorem syl6ib 253

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 218	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3g  297  exlimd  2218  cbvexdw  2359  ax13lem2  2394  cbvexd  2429  axc14  2486  mo3  2648  2eu3  2738  2eu6  2742  necon2bd  3032  necon2d  3039  necon4d  3040  vtoclgft  3545  spcimgft  3578  spc3egv  3596  reupick  4275  prneimg  4771  invdisj  5036  trin  5168  pwssun  5442  wefrc  5535  eqbrrdva  5726  elreldm  5791  elinxp  5876  xp11  6018  ssrnres  6021  suc11  6280  opelf  6525  dffo4  6855  onmindif2  7513  dftpos3  7896  swoer  8305  domtriord  8649  nneneq  8686  unblem1  8756  supnub  8912  infnlb  8942  en3lplem2  9062  suc11reg  9068  inf3lem2  9078  trcl  9156  tz9.13  9206  acndom  9463  carduniima  9508  cardinfima  9509  dfac5lem5  9539  fin23lem26  9733  hsmexlem2  9835  axcc4  9847  axdc3lem2  9859  axdclem2  9928  entric  9965  alephval2  9980  cfpwsdom  9992  fpwwe2lem9  10046  ltapr  10453  supsrlem  10519  sup2  11583  nnunb  11880  nneo  12053  indstr  12303  mul2lt0bi  12482  ngtmnft  12546  qsqueeze  12581  qextlt  12583  qextle  12584  icoshft  12848  injresinj  13148  swrdccatin2  14076  rexuzre  14697  rexico  14698  summo  15059  rpnnen2lem12  15563  divalglem5  15731  ndvdssub  15743  isprm7  16035  pc2dvds  16198  infpn2  16232  vdwnnlem3  16316  mreiincl  16850  intopsn  17847  pmtrrn2  18571  psgnunilem4  18608  ablfac1eulem  19177  lbsextlem3  19915  xrsdsreclb  20575  znleval  20684  elcls3  21674  isclo2  21679  tgcn  21843  cnprest  21880  ordthaus  21975  hauscmplem  21997  comppfsc  22123  kgencn2  22148  prdstopn  22219  xkohaus  22244  qtoptop2  22290  tgqtop  22303  filufint  22511  fclsbas  22612  alexsubALTlem3  22640  alexsubALTlem4  22641  ptcmplem2  22644  cldsubg  22702  isucn2  22871  metequiv2  23103  bcthlem5  23914  vieta1  24887  aannenlem2  24904  ulmbdd  24972  angpined  25394  rlimcnp2  25530  amgm  25554  ftalem3  25638  bposlem6  25851  uhgrvd00  27302  pthdlem2lem  27534  frcond2  28030  lnon0  28559  ocnel  29059  h1dn0  29313  cnlnssadj  29841  cvnbtwn2  30048  cvnbtwn3  30049  cvnbtwn4  30050  dmdbr2  30064  dmdbr3  30066  dmdbr4  30067  superpos  30115  atcvati  30147  mdsymlem4  30167  sumdmdii  30176  cdj3lem1  30195  elicoelioo  30487  archiabl  30834  bnj1280  32299  cusgr3cyclex  32390  loop1cycl  32391  erdszelem9  32453  satfvsucsuc  32619  untangtr  32947  3orel2  32948  dfon2lem6  33040  dfon2lem7  33041  frrlem13  33142  nofv  33171  sltres  33176  noetalem3  33226  outsideofrflx  33595  trer  33671  elicc3  33672  nn0prpw  33678  bj-syl66ib  33897  bj-cbvexdv  34129  bj-sblem1  34173  bj-spcimdv  34227  bj-spcimdvv  34228  topdifinffinlem  34644  icorempo  34648  isbasisrelowllem1  34652  relowlpssretop  34661  difunieq  34671  fvineqsneq  34709  wl-mo3t  34846  poimirlem23  34949  poimirlem29  34955  poimirlem32  34958  poimir  34959  mblfinlem2  34964  sdclem1  35050  fdc  35052  incsequz  35055  rngosn3  35234  0rngo  35337  dmncan1  35386  bicomdd  36022  prtlem15  36043  lsatcvat  36218  lfl1  36238  hlrelat2  36571  cvrat  36590  linepsubN  36920  2llnma3r  36956  dihjatcclem4  38589  dochexmidlem1  38628  sn-dtru  39186  rngunsnply  39865  mptrcllem  40063  frege124d  40196  frege77  40376  frege116  40415  or3or  40461  clsk1indlem3  40483  ssralv2  40955  truniALT  40965  onfrALTlem3  40968  onfrALTlem2  40970  onfrALTlem1  40972  ax6e2ndeq  40983  stoweidlem62  42437  atbiffatnnb  43238  2reu3  43399  2reuimp  43404  gbowge7  44013  gbege6  44015  copisnmnd  44161  line2ylem  44823  line2xlem  44825  setrec1lem4  44878