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

Theorem syl6ib 239
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 204 . 2 (𝜒𝜃)
41, 3syl6 34 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3imtr3g  282  exp4aOLD  631  mtord  689  19.23v  1888  exlimd  2073  exlimdOLD  2210  cbvexd  2265  ax13lem2  2283  axc14  2359  mo3  2494  2eu3  2542  2eu6  2545  exists2  2549  necon2bd  2797  necon2d  2804  necon4d  2805  spcimgft  3256  eqsbc3rOLD  3459  reupick  3869  prneimg  4323  invdisj  4565  trin  4685  pwssun  4934  wefrc  5022  eqbrrdva  5201  elreldm  5258  elres  5342  xp11  5474  ssrnres  5477  ordtri3OLD  5663  suc11  5734  opelf  5964  dffo4  6268  onmindif2  6881  dftpos3  7234  swoer  7636  mapsn  7762  domtriord  7968  nneneq  8005  unblem1  8074  supnub  8228  infnlb  8258  en3lplem2  8372  suc11reg  8376  inf3lem2  8386  trcl  8464  tz9.13  8514  acndom  8734  carduniima  8779  cardinfima  8780  dfac5lem5  8810  fin23lem26  9007  hsmexlem2  9109  axcc4  9121  axdc3lem2  9133  axdclem2  9202  entric  9235  alephval2  9250  cfpwsdom  9262  fpwwe2lem9  9316  ltapr  9723  supsrlem  9788  sup2  10828  nnunb  11135  nneo  11293  indstr  11588  mul2lt0bi  11768  ngtmnft  11831  qsqueeze  11865  qextlt  11867  qextle  11868  icoshft  12121  injresinj  12406  rexuzre  13886  rexico  13887  summo  14241  rpnnen2lem12  14739  divalglem5  14904  ndvdssub  14917  isprm7  15204  pc2dvds  15367  infpn2  15401  vdwnnlem3  15485  mreiincl  16025  intopsn  17022  pmtrrn2  17649  psgnunilem4  17686  ablfac1eulem  18240  lbsextlem3  18927  xrsdsreclb  19558  znleval  19667  elcls3  20639  isclo2  20644  tgcn  20808  cnprest  20845  ordthaus  20940  hauscmplem  20961  comppfsc  21087  kgencn2  21112  prdstopn  21183  xkohaus  21208  qtoptop2  21254  tgqtop  21267  filufint  21476  fclsbas  21577  alexsubALTlem3  21605  alexsubALTlem4  21606  ptcmplem2  21609  cldsubg  21666  isucn2  21835  metequiv2  22066  bcthlem5  22850  vieta1  23788  aannenlem2  23805  ulmbdd  23873  angpined  24274  rlimcnp2  24410  amgm  24434  ftalem3  24518  bposlem6  24731  cusgrares  25767  frgraun  26289  usgreg2spot  26360  lnon0  26843  ocnel  27347  h1dn0  27601  cnlnssadj  28129  cvnbtwn2  28336  cvnbtwn3  28337  cvnbtwn4  28338  dmdbr2  28352  dmdbr3  28354  dmdbr4  28355  superpos  28403  atcvati  28435  mdsymlem4  28455  sumdmdii  28464  cdj3lem1  28483  elicoelioo  28736  archiabl  28889  bnj1280  30148  erdszelem9  30241  untangtr  30651  3orel2  30653  dfon2lem6  30743  dfon2lem7  30744  nofv  30860  sltres  30867  nodenselem4  30889  nodenselem7  30892  outsideofrflx  31210  trer  31286  elicc3  31287  nn0prpw  31294  bj-cbvexdv  31729  bj-spcimdv  31874  topdifinffinlem  32167  icorempt2  32171  isbasisrelowllem1  32175  relowlpssretop  32184  wl-mo3t  32333  poimirlem23  32398  poimirlem29  32404  poimirlem32  32407  poimir  32408  mblfinlem2  32413  sdclem1  32505  fdc  32507  incsequz  32510  rngosn3  32689  0rngo  32792  dmncan1  32841  bicomdd  32949  prtlem15  32974  lsatcvat  33151  lfl1  33171  hlrelat2  33503  cvrat  33522  linepsubN  33852  2llnma3r  33888  dihjatcclem4  35524  dochexmidlem1  35563  rngunsnply  36558  mptrcllem  36735  frege124d  36868  frege77  37050  frege116  37089  or3or  37135  clsk1indlem3  37157  ssralv2  37554  truniALT  37568  onfrALTlem3  37576  onfrALTlem2  37578  onfrALTlem1  37580  ax6e2ndeq  37592  stoweidlem62  38752  atbiffatnnb  39525  2reu3  39634  gboge7  39983  gbege6  39985  upgredg  40365  uhgrvd00  40745  pthdlem2lem  40968  frcond2  41434  copisnmnd  41594
  Copyright terms: Public domain W3C validator