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

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
StepHypRef Expression
1 syl6ib.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6ib.2 . . 3 (𝜒𝜃)
32biimpi 219 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
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  2217  cbvexdw  2351  ax13lem2  2386  cbvexd  2421  axc14  2478  mo3  2626  2eu3  2718  2eu6  2722  necon2bd  3006  necon2d  3013  necon4d  3014  vtoclgft  3504  spcimgft  3537  spc3egv  3555  reupick  4242  prneimg  4748  invdisj  5017  trin  5149  pwssun  5424  wefrc  5517  eqbrrdva  5708  elreldm  5773  elinxp  5860  xp11  6003  ssrnres  6006  suc11  6266  opelf  6517  dffo4  6850  onmindif2  7511  dftpos3  7897  swoer  8306  domtriord  8651  nneneq  8688  unblem1  8758  supnub  8914  infnlb  8944  en3lplem2  9064  suc11reg  9070  inf3lem2  9080  trcl  9158  tz9.13  9208  acndom  9466  carduniima  9511  cardinfima  9512  dfac5lem5  9542  fin23lem26  9740  hsmexlem2  9842  axcc4  9854  axdc3lem2  9866  axdclem2  9935  entric  9972  alephval2  9987  cfpwsdom  9999  fpwwe2lem9  10053  ltapr  10460  supsrlem  10526  sup2  11588  nnunb  11885  nneo  12058  indstr  12308  mul2lt0bi  12487  ngtmnft  12551  qsqueeze  12586  qextlt  12588  qextle  12589  icoshft  12855  injresinj  13157  swrdccatin2  14086  rexuzre  14707  rexico  14708  summo  15069  rpnnen2lem12  15573  divalglem5  15741  ndvdssub  15753  isprm7  16045  pc2dvds  16208  infpn2  16242  vdwnnlem3  16326  mreiincl  16862  intopsn  17859  pmtrrn2  18583  psgnunilem4  18620  ablfac1eulem  19190  lbsextlem3  19928  xrsdsreclb  20141  znleval  20249  elcls3  21691  isclo2  21696  tgcn  21860  cnprest  21897  ordthaus  21992  hauscmplem  22014  comppfsc  22140  kgencn2  22165  prdstopn  22236  xkohaus  22261  qtoptop2  22307  tgqtop  22320  filufint  22528  fclsbas  22629  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem2  22661  cldsubg  22719  isucn2  22888  metequiv2  23120  bcthlem5  23935  vieta1  24911  aannenlem2  24928  ulmbdd  24996  angpined  25419  rlimcnp2  25555  amgm  25579  ftalem3  25663  bposlem6  25876  uhgrvd00  27327  pthdlem2lem  27559  frcond2  28055  lnon0  28584  ocnel  29084  h1dn0  29338  cnlnssadj  29866  cvnbtwn2  30073  cvnbtwn3  30074  cvnbtwn4  30075  dmdbr2  30089  dmdbr3  30091  dmdbr4  30092  superpos  30140  atcvati  30172  mdsymlem4  30192  sumdmdii  30201  cdj3lem1  30220  elicoelioo  30530  archiabl  30880  bnj1280  32400  cusgr3cyclex  32491  loop1cycl  32492  erdszelem9  32554  satfvsucsuc  32720  untangtr  33048  3orel2  33049  dfon2lem6  33141  dfon2lem7  33142  frrlem13  33243  nofv  33272  sltres  33277  noetalem3  33327  outsideofrflx  33696  trer  33772  elicc3  33773  nn0prpw  33779  bj-syl66ib  33998  bj-cbvexdv  34232  bj-sblem1  34276  bj-spcimdv  34330  bj-spcimdvv  34331  topdifinffinlem  34759  icorempo  34763  isbasisrelowllem1  34767  relowlpssretop  34776  difunieq  34786  fvineqsneq  34824  wl-mo3t  34970  poimirlem23  35073  poimirlem29  35079  poimirlem32  35082  poimir  35083  mblfinlem2  35088  sdclem1  35174  fdc  35176  incsequz  35179  rngosn3  35355  0rngo  35458  dmncan1  35507  bicomdd  36143  prtlem15  36164  lsatcvat  36339  lfl1  36359  hlrelat2  36692  cvrat  36711  linepsubN  37041  2llnma3r  37077  dihjatcclem4  38710  dochexmidlem1  38749  sn-dtru  39390  sn-sup2  39581  rngunsnply  40104  mptrcllem  40300  frege124d  40449  frege77  40628  frege116  40667  or3or  40711  clsk1indlem3  40733  ssralv2  41224  truniALT  41234  onfrALTlem3  41237  onfrALTlem2  41239  onfrALTlem1  41241  ax6e2ndeq  41252  stoweidlem62  42691  atbiffatnnb  43492  2reu3  43653  2reuimp  43658  gbowge7  44268  gbege6  44270  copisnmnd  44416  line2ylem  45152  line2xlem  45154  setrec1lem4  45207
  Copyright terms: Public domain W3C validator