Theorem syl6ib 241

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

Hypotheses

Ref	Expression
syl6ib.1	|- ( ph -> ( ps -> ch ) )
syl6ib.2	|- ( ch <-> th )

Assertion

Ref	Expression
syl6ib	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6ib.2	. . 3 |- ( ch <-> th )
3	2	biimpi 206	. 2 |- ( ch -> th )
4	1, 3	syl6 35	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 196

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 197

This theorem is referenced by:  3imtr3g  284  exp4aOLD  634  mtord  692  19.23v  1902  exlimd  2087  exlimdOLD  2223  cbvexd  2278  ax13lem2  2296  axc14  2372  mo3  2507  2eu3  2555  2eu6  2558  exists2  2562  necon2bd  2810  necon2d  2817  necon4d  2818  spcimgft  3284  eqsbc3rOLD  3493  reupick  3911  prneimg  4388  invdisj  4638  trin  4763  pwssun  5020  wefrc  5108  eqbrrdva  5291  elreldm  5350  elres  5435  xp11  5569  ssrnres  5572  ordtri3OLD  5760  suc11  5831  opelf  6065  dffo4  6375  onmindif2  7012  dftpos3  7370  swoer  7772  mapsn  7899  domtriord  8106  nneneq  8143  unblem1  8212  supnub  8368  infnlb  8398  en3lplem2  8512  suc11reg  8516  inf3lem2  8526  trcl  8604  tz9.13  8654  acndom  8874  carduniima  8919  cardinfima  8920  dfac5lem5  8950  fin23lem26  9147  hsmexlem2  9249  axcc4  9261  axdc3lem2  9273  axdclem2  9342  entric  9379  alephval2  9394  cfpwsdom  9406  fpwwe2lem9  9460  ltapr  9867  supsrlem  9932  sup2  10979  nnunb  11288  nneo  11461  indstr  11756  mul2lt0bi  11936  ngtmnft  11997  qsqueeze  12032  qextlt  12034  qextle  12035  icoshft  12294  injresinj  12589  rexuzre  14092  rexico  14093  summo  14448  rpnnen2lem12  14954  divalglem5  15120  ndvdssub  15133  isprm7  15420  pc2dvds  15583  infpn2  15617  vdwnnlem3  15701  mreiincl  16256  intopsn  17253  pmtrrn2  17880  psgnunilem4  17917  ablfac1eulem  18471  lbsextlem3  19160  xrsdsreclb  19793  znleval  19903  elcls3  20887  isclo2  20892  tgcn  21056  cnprest  21093  ordthaus  21188  hauscmplem  21209  comppfsc  21335  kgencn2  21360  prdstopn  21431  xkohaus  21456  qtoptop2  21502  tgqtop  21515  filufint  21724  fclsbas  21825  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem2  21857  cldsubg  21914  isucn2  22083  metequiv2  22315  bcthlem5  23125  vieta1  24067  aannenlem2  24084  ulmbdd  24152  angpined  24557  rlimcnp2  24693  amgm  24717  ftalem3  24801  bposlem6  25014  uhgrvd00  26430  pthdlem2lem  26663  frcond2  27131  lnon0  27653  ocnel  28157  h1dn0  28411  cnlnssadj  28939  cvnbtwn2  29146  cvnbtwn3  29147  cvnbtwn4  29148  dmdbr2  29162  dmdbr3  29164  dmdbr4  29165  superpos  29213  atcvati  29245  mdsymlem4  29265  sumdmdii  29274  cdj3lem1  29293  elicoelioo  29540  archiabl  29752  bnj1280  31088  erdszelem9  31181  untangtr  31591  3orel2  31592  dfon2lem6  31693  dfon2lem7  31694  nofv  31810  sltres  31815  noetalem3  31865  outsideofrflx  32234  trer  32310  elicc3  32311  nn0prpw  32318  bj-cbvexdv  32736  bj-syl66ib  32833  bj-spcimdv  32884  bj-spcimdvv  32885  topdifinffinlem  33195  icorempt2  33199  isbasisrelowllem1  33203  relowlpssretop  33212  wl-mo3t  33358  poimirlem23  33432  poimirlem29  33438  poimirlem32  33441  poimir  33442  mblfinlem2  33447  sdclem1  33539  fdc  33541  incsequz  33544  rngosn3  33723  0rngo  33826  dmncan1  33875  bicomdd  34138  prtlem15  34160  lsatcvat  34337  lfl1  34357  hlrelat2  34689  cvrat  34708  linepsubN  35038  2llnma3r  35074  dihjatcclem4  36710  dochexmidlem1  36749  rngunsnply  37743  mptrcllem  37920  frege124d  38053  frege77  38234  frege116  38273  or3or  38319  clsk1indlem3  38341  ssralv2  38737  truniALT  38751  onfrALTlem3  38759  onfrALTlem2  38761  onfrALTlem1  38763  ax6e2ndeq  38775  stoweidlem62  40279  atbiffatnnb  41079  2reu3  41188  gbowge7  41651  gbege6  41653  copisnmnd  41809  setrec1lem4  42437