Theorem syl6ib 250

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 215	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	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:  3imtr3g  294  3orel2  1484  exlimd  2210  cbvexdw  2335  ax13lem2  2374  cbvexd  2406  axc14  2461  mo3  2562  2eu3  2653  2eu6  2656  necon2bd  2956  necon2d  2963  necon4d  2964  vtoclgft  3501  spcimgft  3535  spc3egv  3551  elabgt  3613  reupick  4265  prneimg  4799  dfiun2g  4977  invdisj  5076  trin  5221  exexneq  5379  pwssun  5515  wefrc  5614  eqbrrdva  5811  elreldm  5876  elinxp  5961  xp11  6113  ssrnres  6116  suc11  6407  opelf  6686  dffo4  7035  onmindif2  7720  dftpos3  8130  frrlem13  8184  swoer  8599  domtriord  8988  nneneq  9074  nneneqOLD  9086  unblem1  9160  supnub  9319  infnlb  9349  en3lplem2  9470  suc11reg  9476  inf3lem2  9486  trcl  9585  tz9.13  9648  acndom  9908  carduniima  9953  cardinfima  9954  dfac5lem5  9984  fin23lem26  10182  hsmexlem2  10284  axcc4  10296  axdc3lem2  10308  axdclem2  10377  entric  10414  alephval2  10429  cfpwsdom  10441  fpwwe2lem8  10495  ltapr  10902  supsrlem  10968  sup2  12032  nnunb  12330  nneo  12505  indstr  12757  mul2lt0bi  12937  ngtmnft  13001  qsqueeze  13036  qextlt  13038  qextle  13039  icoshft  13306  injresinj  13609  swrdccatin2  14540  rexuzre  15163  rexico  15164  summo  15528  rpnnen2lem12  16033  divalglem5  16205  ndvdssub  16217  isprm7  16510  prmdvdsncoprmbd  16528  pc2dvds  16677  infpn2  16711  vdwnnlem3  16795  mreiincl  17402  intopsn  18435  pmtrrn2  19164  psgnunilem4  19201  ablfac1eulem  19770  lbsextlem3  20528  xrsdsreclb  20751  znleval  20868  elcls3  22340  isclo2  22345  tgcn  22509  cnprest  22546  ordthaus  22641  hauscmplem  22663  comppfsc  22789  kgencn2  22814  prdstopn  22885  xkohaus  22910  qtoptop2  22956  tgqtop  22969  filufint  23177  fclsbas  23278  alexsubALTlem3  23306  alexsubALTlem4  23307  ptcmplem2  23310  cldsubg  23368  isucn2  23537  metequiv2  23772  bcthlem5  24598  vieta1  25578  aannenlem2  25595  ulmbdd  25663  angpined  26086  rlimcnp2  26222  amgm  26246  ftalem3  26330  bposlem6  26543  nofv  26911  sltres  26916  nogt01o  26950  nosupprefixmo  26954  noinfprefixmo  26955  noetasuplem4  26990  uhgrvd00  28190  pthdlem2lem  28423  frcond2  28919  lnon0  29448  ocnel  29948  h1dn0  30202  cnlnssadj  30730  cvnbtwn2  30937  cvnbtwn3  30938  cvnbtwn4  30939  dmdbr2  30953  dmdbr3  30955  dmdbr4  30956  superpos  31004  atcvati  31036  mdsymlem4  31056  sumdmdii  31065  cdj3lem1  31084  elicoelioo  31386  archiabl  31739  bnj1280  33299  cusgr3cyclex  33397  loop1cycl  33398  erdszelem9  33460  satfvsucsuc  33626  untangtr  33954  dfon2lem6  34047  dfon2lem7  34048  outsideofrflx  34525  trer  34601  elicc3  34602  nn0prpw  34608  bj-syl66ib  34831  bj-cbvexdv  35078  bj-sblem1  35121  bj-spcimdv  35175  bj-spcimdvv  35176  topdifinffinlem  35623  icorempo  35627  isbasisrelowllem1  35631  relowlpssretop  35640  difunieq  35650  fvineqsneq  35688  wl-mo3t  35836  poimirlem23  35905  poimirlem29  35911  poimirlem32  35914  poimir  35915  mblfinlem2  35920  sdclem1  36006  fdc  36008  incsequz  36011  rngosn3  36187  0rngo  36290  dmncan1  36339  disjdmqscossss  37070  bicomdd  37121  prtlem15  37142  lsatcvat  37317  lfl1  37337  hlrelat2  37671  cvrat  37690  linepsubN  38020  2llnma3r  38056  dihjatcclem4  39689  dochexmidlem1  39728  sn-sup2  40699  rngunsnply  41261  mptrcllem  41542  frege124d  41690  frege77  41869  frege116  41908  or3or  41952  clsk1indlem3  41974  ssralv2  42472  truniALT  42482  onfrALTlem3  42485  onfrALTlem2  42487  onfrALTlem1  42489  ax6e2ndeq  42500  stoweidlem62  43939  atbiffatnnb  44758  2reu3  44953  2reuimp  44958  gbowge7  45566  gbege6  45568  copisnmnd  45714  line2ylem  46448  line2xlem  46450  setrec1lem4  46747