MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6ib Structured version   Unicode version

Theorem syl6ib 226
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
StepHypRef Expression
1 syl6ib.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6ib.2 . . 3  |-  ( ch  <->  th )
32biimpi 194 . 2  |-  ( ch 
->  th )
41, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr3g  269  exp4a  606  mtord  660  exlimd  1847  cbvexd  1974  axc9lem2  1988  equveliOLD  2039  axc14  2063  mo3  2298  2eu3  2367  2eu6  2371  exists2  2377  necon2bd  2659  necon2d  2660  necon4ad  2671  necon4d  2673  necon1bd  2678  spcimgft  3047  eqsbc3r  3247  reupick  3633  prneimg  4052  invdisj  4280  trin  4394  pwssun  4626  wefrc  4713  ordtri3  4754  suc11  4821  eqbrrdva  5008  elreldm  5063  elres  5144  xp11  5272  ssrnres  5275  opelf  5573  dffo4  5858  onmindif2  6422  dftpos3  6762  swoer  7128  mapsn  7253  domtriord  7456  nneneq  7493  unblem1  7563  supnub  7711  en3lplem2  7820  suc11reg  7824  inf3lem2  7834  trcl  7947  tz9.13  7997  acndom  8220  carduniima  8265  cardinfima  8266  dfac5lem5  8296  fin23lem26  8493  hsmexlem2  8595  axcc4  8607  axdc3lem2  8619  axdclem2  8688  entric  8720  alephval2  8735  cfpwsdom  8747  fpwwe2lem9  8804  ltapr  9213  supsrlem  9277  sup2  10285  nnunb  10574  nneo  10724  indstr  10922  ngtmnft  11138  qsqueeze  11170  qextlt  11172  qextle  11173  icoshft  11406  injresinj  11638  rexuzre  12839  rexico  12840  summo  13193  rpnnen2  13507  divalglem5  13600  ndvdssub  13610  pc2dvds  13944  infpn2  13973  vdwnnlem3  14057  mreiincl  14533  pmtrrn2  15965  psgnunilem4  16002  ablfac1eulem  16572  lbsextlem3  17240  xrsdsreclb  17859  znleval  17986  elcls3  18686  isclo2  18691  tgcn  18855  cnprest  18892  ordthaus  18987  hauscmplem  19008  kgencn2  19129  prdstopn  19200  xkohaus  19225  qtoptop2  19271  filufint  19492  fclsbas  19593  alexsubALTlem3  19620  alexsubALTlem4  19621  ptcmplem2  19624  cldsubg  19680  isucn2  19853  metequiv2  20084  bcthlem5  20838  vieta1  21777  aannenlem2  21794  ulmbdd  21862  angpined  22224  rlimcnp2  22359  amgm  22383  ftalem3  22411  bposlem6  22627  cusgrares  23379  rngosn3  23912  lnon0  24197  ocnel  24700  h1dn0  24954  cnlnssadj  25483  cvnbtwn2  25690  cvnbtwn3  25691  cvnbtwn4  25692  dmdbr2  25706  dmdbr3  25708  dmdbr4  25709  superpos  25757  atcvati  25789  mdsymlem4  25809  sumdmdii  25818  cdj3lem1  25837  mul2lt0bi  26041  elicoelioo  26067  archiabl  26214  erdszelem9  27086  untangtr  27364  3orel2  27366  dfon2lem6  27600  dfon2lem7  27601  nofv  27797  sltres  27804  nodenselem4  27824  nodenselem7  27827  outsideofrflx  28157  wl-mo3t  28395  mblfinlem2  28427  trer  28509  elicc3  28510  nn0prpw  28516  comppfsc  28577  sdclem1  28637  fdc  28639  incsequz  28642  0rngo  28825  dmncan1  28874  exlimddvf  28927  bicomdd  28985  prtlem90  29000  prtlem15  29018  rngunsnply  29528  stoweidlem62  29855  atbiffatnnb  29925  2reu3  30010  frgraun  30586  usgreg2spot  30658  ssralv2  31234  truniALT  31246  onfrALTlem3  31250  onfrALTlem2  31252  onfrALTlem1  31254  ax6e2ndeq  31266  bnj1280  32009  bj-cbvexdv  32235  lsatcvat  32693  lfl1  32713  hlrelat2  33045  cvrat  33064  linepsubN  33394  2llnma3r  33430  dihjatcclem4  35064  dochexmidlem1  35103
  Copyright terms: Public domain W3C validator