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

Theorem syl6ib 241
 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 206 . 2 (𝜒𝜃)
41, 3syl6 35 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196 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 197 This theorem is referenced by:  3imtr3g  284  exp4aOLD  633  mtord  691  19.23v  1899  exlimd  2085  exlimdOLD  2222  cbvexd  2277  ax13lem2  2295  axc14  2371  mo3  2506  2eu3  2554  2eu6  2557  exists2  2561  necon2bd  2806  necon2d  2813  necon4d  2814  spcimgft  3274  eqsbc3rOLD  3480  reupick  3893  prneimg  4363  invdisj  4611  trin  4733  pwssun  4990  wefrc  5078  eqbrrdva  5261  elreldm  5320  elres  5404  xp11  5538  ssrnres  5541  ordtri3OLD  5729  suc11  5800  opelf  6032  dffo4  6341  onmindif2  6974  dftpos3  7330  swoer  7732  mapsn  7859  domtriord  8066  nneneq  8103  unblem1  8172  supnub  8328  infnlb  8358  en3lplem2  8472  suc11reg  8476  inf3lem2  8486  trcl  8564  tz9.13  8614  acndom  8834  carduniima  8879  cardinfima  8880  dfac5lem5  8910  fin23lem26  9107  hsmexlem2  9209  axcc4  9221  axdc3lem2  9233  axdclem2  9302  entric  9339  alephval2  9354  cfpwsdom  9366  fpwwe2lem9  9420  ltapr  9827  supsrlem  9892  sup2  10939  nnunb  11248  nneo  11421  indstr  11716  mul2lt0bi  11896  ngtmnft  11957  qsqueeze  11991  qextlt  11993  qextle  11994  icoshft  12252  injresinj  12545  rexuzre  14042  rexico  14043  summo  14397  rpnnen2lem12  14898  divalglem5  15063  ndvdssub  15076  isprm7  15363  pc2dvds  15526  infpn2  15560  vdwnnlem3  15644  mreiincl  16196  intopsn  17193  pmtrrn2  17820  psgnunilem4  17857  ablfac1eulem  18411  lbsextlem3  19100  xrsdsreclb  19733  znleval  19843  elcls3  20827  isclo2  20832  tgcn  20996  cnprest  21033  ordthaus  21128  hauscmplem  21149  comppfsc  21275  kgencn2  21300  prdstopn  21371  xkohaus  21396  qtoptop2  21442  tgqtop  21455  filufint  21664  fclsbas  21765  alexsubALTlem3  21793  alexsubALTlem4  21794  ptcmplem2  21797  cldsubg  21854  isucn2  22023  metequiv2  22255  bcthlem5  23065  vieta1  24005  aannenlem2  24022  ulmbdd  24090  angpined  24491  rlimcnp2  24627  amgm  24651  ftalem3  24735  bposlem6  24948  uhgrvd00  26350  pthdlem2lem  26566  frcond2  27031  lnon0  27541  ocnel  28045  h1dn0  28299  cnlnssadj  28827  cvnbtwn2  29034  cvnbtwn3  29035  cvnbtwn4  29036  dmdbr2  29050  dmdbr3  29052  dmdbr4  29053  superpos  29101  atcvati  29133  mdsymlem4  29153  sumdmdii  29162  cdj3lem1  29181  elicoelioo  29425  archiabl  29579  bnj1280  30849  erdszelem9  30942  untangtr  31352  3orel2  31354  dfon2lem6  31447  dfon2lem7  31448  nofv  31564  sltres  31571  nodenselem4  31600  nodenselem7  31603  noprefixmo  31626  outsideofrflx  31929  trer  32005  elicc3  32006  nn0prpw  32013  bj-cbvexdv  32431  bj-syl66ib  32531  bj-spcimdv  32584  bj-spcimdvv  32585  topdifinffinlem  32866  icorempt2  32870  isbasisrelowllem1  32874  relowlpssretop  32883  wl-mo3t  33029  poimirlem23  33103  poimirlem29  33109  poimirlem32  33112  poimir  33113  mblfinlem2  33118  sdclem1  33210  fdc  33212  incsequz  33215  rngosn3  33394  0rngo  33497  dmncan1  33546  bicomdd  33654  prtlem15  33679  lsatcvat  33856  lfl1  33876  hlrelat2  34208  cvrat  34227  linepsubN  34557  2llnma3r  34593  dihjatcclem4  36229  dochexmidlem1  36268  rngunsnply  37263  mptrcllem  37440  frege124d  37573  frege77  37755  frege116  37794  or3or  37840  clsk1indlem3  37862  ssralv2  38258  truniALT  38272  onfrALTlem3  38280  onfrALTlem2  38282  onfrALTlem1  38284  ax6e2ndeq  38296  stoweidlem62  39616  atbiffatnnb  40413  2reu3  40522  gboge7  40976  gbege6  40978  copisnmnd  41127  setrec1lem4  41760
 Copyright terms: Public domain W3C validator