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

Theorem syl6ib 243
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 208 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  3imtr3g  287  mtord  863  exlimd  2148  ax13lem2  2305  cbvexd  2342  axc14  2400  mo3  2577  mo3OLD  2578  2eu3  2685  2eu3OLD  2686  2eu6  2689  exists2OLD  2696  necon2bd  2977  necon2d  2984  necon4d  2985  spcimgft  3499  spc3egv  3516  reupick  4168  prneimg  4653  invdisj  4909  trin  5034  pwssun  5302  wefrc  5395  eqbrrdva  5584  elreldm  5642  elinxp  5729  xp11  5866  ssrnres  5869  suc11  6126  opelf  6362  dffo4  6686  onmindif2  7337  dftpos3  7707  swoer  8113  domtriord  8453  nneneq  8490  unblem1  8559  supnub  8715  infnlb  8745  en3lplem2  8864  suc11reg  8870  inf3lem2  8880  trcl  8958  tz9.13  9008  acndom  9265  carduniima  9310  cardinfima  9311  dfac5lem5  9341  fin23lem26  9539  hsmexlem2  9641  axcc4  9653  axdc3lem2  9665  axdclem2  9734  entric  9771  alephval2  9786  cfpwsdom  9798  fpwwe2lem9  9852  ltapr  10259  supsrlem  10325  sup2  11392  nnunb  11697  nneo  11873  indstr  12124  mul2lt0bi  12306  ngtmnft  12370  qsqueeze  12405  qextlt  12407  qextle  12408  icoshft  12669  injresinj  12967  rexuzre  14567  rexico  14568  summo  14928  rpnnen2lem12  15432  divalglem5  15602  ndvdssub  15614  isprm7  15902  pc2dvds  16065  infpn2  16099  vdwnnlem3  16183  mreiincl  16719  intopsn  17715  pmtrrn2  18343  psgnunilem4  18381  ablfac1eulem  18938  lbsextlem3  19648  xrsdsreclb  20288  znleval  20397  elcls3  21389  isclo2  21394  tgcn  21558  cnprest  21595  ordthaus  21690  hauscmplem  21712  comppfsc  21838  kgencn2  21863  prdstopn  21934  xkohaus  21959  qtoptop2  22005  tgqtop  22018  filufint  22226  fclsbas  22327  alexsubALTlem3  22355  alexsubALTlem4  22356  ptcmplem2  22359  cldsubg  22416  isucn2  22585  metequiv2  22817  bcthlem5  23628  vieta1  24598  aannenlem2  24615  ulmbdd  24683  angpined  25103  rlimcnp2  25240  amgm  25264  ftalem3  25348  bposlem6  25561  uhgrvd00  27013  pthdlem2lem  27250  frcond2  27795  lnon0  28346  ocnel  28850  h1dn0  29104  cnlnssadj  29632  cvnbtwn2  29839  cvnbtwn3  29840  cvnbtwn4  29841  dmdbr2  29855  dmdbr3  29857  dmdbr4  29858  superpos  29906  atcvati  29938  mdsymlem4  29958  sumdmdii  29967  cdj3lem1  29986  elicoelioo  30254  archiabl  30493  bnj1280  31937  erdszelem9  32031  untangtr  32460  3orel2  32461  dfon2lem6  32553  dfon2lem7  32554  frrlem13  32656  nofv  32685  sltres  32690  noetalem3  32740  outsideofrflx  33109  trer  33185  elicc3  33186  nn0prpw  33192  bj-syl66ib  33407  bj-cbvexdv  33581  bj-sblem1  33657  bj-spcimdv  33704  bj-spcimdvv  33705  topdifinffinlem  34070  icorempo  34074  isbasisrelowllem1  34078  relowlpssretop  34087  difunieq  34097  fvineqsneq  34134  wl-mo3t  34253  poimirlem23  34356  poimirlem29  34362  poimirlem32  34365  poimir  34366  mblfinlem2  34371  sdclem1  34460  fdc  34462  incsequz  34465  rngosn3  34644  0rngo  34747  dmncan1  34796  bicomdd  35435  prtlem15  35456  lsatcvat  35631  lfl1  35651  hlrelat2  35984  cvrat  36003  linepsubN  36333  2llnma3r  36369  dihjatcclem4  38002  dochexmidlem1  38041  sn-dtru  38556  rngunsnply  39169  mptrcllem  39336  frege124d  39469  frege77  39649  frege116  39688  or3or  39734  clsk1indlem3  39756  ssralv2  40284  truniALT  40294  onfrALTlem3  40297  onfrALTlem2  40299  onfrALTlem1  40301  ax6e2ndeq  40312  stoweidlem62  41778  atbiffatnnb  42578  2reu3  42715  2reuimp  42720  gbowge7  43296  gbege6  43298  copisnmnd  43444  line2ylem  44106  line2xlem  44108  setrec1lem4  44160
  Copyright terms: Public domain W3C validator