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

Theorem syl6ib 252
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 217 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3imtr3g  296  exlimd  2208  cbvexdw  2350  ax13lem2  2385  cbvexd  2420  axc14  2478  mo3  2641  2eu3  2732  2eu3OLD  2733  2eu6  2737  necon2bd  3029  necon2d  3036  necon4d  3037  vtoclgft  3551  spcimgft  3583  spc3egv  3601  reupick  4284  prneimg  4777  invdisj  5041  trin  5173  pwssun  5448  wefrc  5542  eqbrrdva  5733  elreldm  5798  elinxp  5883  xp11  6025  ssrnres  6028  suc11  6287  opelf  6532  dffo4  6861  onmindif2  7516  dftpos3  7899  swoer  8308  domtriord  8651  nneneq  8688  unblem1  8758  supnub  8914  infnlb  8944  en3lplem2  9064  suc11reg  9070  inf3lem2  9080  trcl  9158  tz9.13  9208  acndom  9465  carduniima  9510  cardinfima  9511  dfac5lem5  9541  fin23lem26  9735  hsmexlem2  9837  axcc4  9849  axdc3lem2  9861  axdclem2  9930  entric  9967  alephval2  9982  cfpwsdom  9994  fpwwe2lem9  10048  ltapr  10455  supsrlem  10521  sup2  11585  nnunb  11881  nneo  12054  indstr  12304  mul2lt0bi  12483  ngtmnft  12547  qsqueeze  12582  qextlt  12584  qextle  12585  icoshft  12847  injresinj  13146  swrdccatin2  14079  rexuzre  14700  rexico  14701  summo  15062  rpnnen2lem12  15566  divalglem5  15736  ndvdssub  15748  isprm7  16040  pc2dvds  16203  infpn2  16237  vdwnnlem3  16321  mreiincl  16855  intopsn  17852  pmtrrn2  18517  psgnunilem4  18554  ablfac1eulem  19123  lbsextlem3  19861  xrsdsreclb  20520  znleval  20629  elcls3  21619  isclo2  21624  tgcn  21788  cnprest  21825  ordthaus  21920  hauscmplem  21942  comppfsc  22068  kgencn2  22093  prdstopn  22164  xkohaus  22189  qtoptop2  22235  tgqtop  22248  filufint  22456  fclsbas  22557  alexsubALTlem3  22585  alexsubALTlem4  22586  ptcmplem2  22589  cldsubg  22646  isucn2  22815  metequiv2  23047  bcthlem5  23858  vieta1  24828  aannenlem2  24845  ulmbdd  24913  angpined  25335  rlimcnp2  25471  amgm  25495  ftalem3  25579  bposlem6  25792  uhgrvd00  27243  pthdlem2lem  27475  frcond2  27973  lnon0  28502  ocnel  29002  h1dn0  29256  cnlnssadj  29784  cvnbtwn2  29991  cvnbtwn3  29992  cvnbtwn4  29993  dmdbr2  30007  dmdbr3  30009  dmdbr4  30010  superpos  30058  atcvati  30090  mdsymlem4  30110  sumdmdii  30119  cdj3lem1  30138  elicoelioo  30427  archiabl  30754  bnj1280  32189  cusgr3cyclex  32280  loop1cycl  32281  erdszelem9  32343  satfvsucsuc  32509  untangtr  32837  3orel2  32838  dfon2lem6  32930  dfon2lem7  32931  frrlem13  33032  nofv  33061  sltres  33066  noetalem3  33116  outsideofrflx  33485  trer  33561  elicc3  33562  nn0prpw  33568  bj-syl66ib  33787  bj-cbvexdv  34019  bj-sblem1  34063  bj-spcimdv  34108  bj-spcimdvv  34109  topdifinffinlem  34510  icorempo  34514  isbasisrelowllem1  34518  relowlpssretop  34527  difunieq  34537  fvineqsneq  34575  wl-mo3t  34693  poimirlem23  34796  poimirlem29  34802  poimirlem32  34805  poimir  34806  mblfinlem2  34811  sdclem1  34899  fdc  34901  incsequz  34904  rngosn3  35083  0rngo  35186  dmncan1  35235  bicomdd  35870  prtlem15  35891  lsatcvat  36066  lfl1  36086  hlrelat2  36419  cvrat  36438  linepsubN  36768  2llnma3r  36804  dihjatcclem4  38437  dochexmidlem1  38476  sn-dtru  38989  rngunsnply  39651  mptrcllem  39851  frege124d  39984  frege77  40164  frege116  40203  or3or  40249  clsk1indlem3  40271  ssralv2  40742  truniALT  40752  onfrALTlem3  40755  onfrALTlem2  40757  onfrALTlem1  40759  ax6e2ndeq  40770  stoweidlem62  42224  atbiffatnnb  43025  2reu3  43186  2reuimp  43191  gbowge7  43805  gbege6  43807  copisnmnd  43953  line2ylem  44666  line2xlem  44668  setrec1lem4  44721
  Copyright terms: Public domain W3C validator