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

Theorem syl6ib 242
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 207 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  3imtr3g  286  mtord  895  19.23vOLD  2082  exlimd  2254  exlimdOLD  2397  cbvexd  2449  ax13lem2  2463  axc14  2531  mo3  2670  2eu3  2719  2eu6  2722  exists2  2726  necon2bd  2994  necon2d  3001  necon4d  3002  spcimgft  3477  reupick  4112  prneimg  4575  invdisj  4830  trin  4956  pwssun  5215  wefrc  5305  eqbrrdva  5493  elreldm  5551  elinxp  5637  elresOLD  5639  xp11  5780  ssrnres  5783  ordtri3OLD  5973  suc11  6044  opelf  6280  dffo4  6597  onmindif2  7242  dftpos3  7605  swoer  8009  domtriord  8345  nneneq  8382  unblem1  8451  supnub  8607  infnlb  8637  en3lplem2  8755  suc11reg  8763  inf3lem2  8773  trcl  8851  tz9.13  8901  acndom  9157  carduniima  9202  cardinfima  9203  dfac5lem5  9233  fin23lem26  9432  hsmexlem2  9534  axcc4  9546  axdc3lem2  9558  axdclem2  9627  entric  9664  alephval2  9679  cfpwsdom  9691  fpwwe2lem9  9745  ltapr  10152  supsrlem  10217  sup2  11264  nnunb  11555  nneo  11727  indstr  11975  mul2lt0bi  12150  ngtmnft  12215  qsqueeze  12250  qextlt  12252  qextle  12253  icoshft  12515  injresinj  12813  rexuzre  14315  rexico  14316  summo  14671  rpnnen2lem12  15174  divalglem5  15340  ndvdssub  15352  isprm7  15637  pc2dvds  15800  infpn2  15834  vdwnnlem3  15918  mreiincl  16461  intopsn  17458  pmtrrn2  18081  psgnunilem4  18118  ablfac1eulem  18673  lbsextlem3  19369  xrsdsreclb  20001  znleval  20110  elcls3  21101  isclo2  21106  tgcn  21270  cnprest  21307  ordthaus  21402  hauscmplem  21423  comppfsc  21549  kgencn2  21574  prdstopn  21645  xkohaus  21670  qtoptop2  21716  tgqtop  21729  filufint  21937  fclsbas  22038  alexsubALTlem3  22066  alexsubALTlem4  22067  ptcmplem2  22070  cldsubg  22127  isucn2  22296  metequiv2  22528  bcthlem5  23337  vieta1  24281  aannenlem2  24298  ulmbdd  24366  angpined  24771  rlimcnp2  24907  amgm  24931  ftalem3  25015  bposlem6  25228  uhgrvd00  26658  pthdlem2lem  26891  frcond2  27442  lnon0  27981  ocnel  28485  h1dn0  28739  cnlnssadj  29267  cvnbtwn2  29474  cvnbtwn3  29475  cvnbtwn4  29476  dmdbr2  29490  dmdbr3  29492  dmdbr4  29493  superpos  29541  atcvati  29573  mdsymlem4  29593  sumdmdii  29602  cdj3lem1  29621  elicoelioo  29867  archiabl  30077  bnj1280  31411  erdszelem9  31504  untangtr  31913  3orel2  31914  dfon2lem6  32013  dfon2lem7  32014  nofv  32131  sltres  32136  noetalem3  32186  outsideofrflx  32555  trer  32631  elicc3  32632  nn0prpw  32639  bj-syl66ib  32856  bj-cbvexdv  33050  bj-spcimdv  33192  bj-spcimdvv  33193  topdifinffinlem  33511  icorempt2  33515  isbasisrelowllem1  33519  relowlpssretop  33528  wl-mo3t  33672  poimirlem23  33745  poimirlem29  33751  poimirlem32  33754  poimir  33755  mblfinlem2  33760  sdclem1  33850  fdc  33852  incsequz  33855  rngosn3  34034  0rngo  34137  dmncan1  34186  bicomdd  34632  prtlem15  34654  lsatcvat  34830  lfl1  34850  hlrelat2  35183  cvrat  35202  linepsubN  35532  2llnma3r  35568  dihjatcclem4  37202  dochexmidlem1  37241  rngunsnply  38244  mptrcllem  38420  frege124d  38553  frege77  38734  frege116  38773  or3or  38819  clsk1indlem3  38841  ssralv2  39235  truniALT  39249  onfrALTlem3  39257  onfrALTlem2  39259  onfrALTlem1  39261  ax6e2ndeq  39273  stoweidlem62  40758  atbiffatnnb  41561  2reu3  41700  gbowge7  42226  gbege6  42228  copisnmnd  42377  setrec1lem4  43005
  Copyright terms: Public domain W3C validator