MPE Home 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  693  19.23vOLD  1959  exlimd  2125  exlimdOLD  2259  cbvexd  2314  ax13lem2  2332  axc14  2400  mo3  2536  2eu3  2584  2eu6  2587  exists2  2591  necon2bd  2839  necon2d  2846  necon4d  2847  spcimgft  3315  eqsbc3rOLD  3526  reupick  3944  prneimg  4419  invdisj  4670  trin  4796  pwssun  5049  wefrc  5137  eqbrrdva  5324  elreldm  5382  elres  5470  xp11  5604  ssrnres  5607  ordtri3OLD  5798  suc11  5869  opelf  6103  dffo4  6415  onmindif2  7054  dftpos3  7415  swoer  7817  mapsn  7941  domtriord  8147  nneneq  8184  unblem1  8253  supnub  8409  infnlb  8439  en3lplem2  8550  suc11reg  8554  inf3lem2  8564  trcl  8642  tz9.13  8692  acndom  8912  carduniima  8957  cardinfima  8958  dfac5lem5  8988  fin23lem26  9185  hsmexlem2  9287  axcc4  9299  axdc3lem2  9311  axdclem2  9380  entric  9417  alephval2  9432  cfpwsdom  9444  fpwwe2lem9  9498  ltapr  9905  supsrlem  9970  sup2  11017  nnunb  11326  nneo  11499  indstr  11794  mul2lt0bi  11974  ngtmnft  12035  qsqueeze  12070  qextlt  12072  qextle  12073  icoshft  12332  injresinj  12629  rexuzre  14136  rexico  14137  summo  14492  rpnnen2lem12  14998  divalglem5  15167  ndvdssub  15180  isprm7  15467  pc2dvds  15630  infpn2  15664  vdwnnlem3  15748  mreiincl  16303  intopsn  17300  pmtrrn2  17926  psgnunilem4  17963  ablfac1eulem  18517  lbsextlem3  19208  xrsdsreclb  19841  znleval  19951  elcls3  20935  isclo2  20940  tgcn  21104  cnprest  21141  ordthaus  21236  hauscmplem  21257  comppfsc  21383  kgencn2  21408  prdstopn  21479  xkohaus  21504  qtoptop2  21550  tgqtop  21563  filufint  21771  fclsbas  21872  alexsubALTlem3  21900  alexsubALTlem4  21901  ptcmplem2  21904  cldsubg  21961  isucn2  22130  metequiv2  22362  bcthlem5  23171  vieta1  24112  aannenlem2  24129  ulmbdd  24197  angpined  24602  rlimcnp2  24738  amgm  24762  ftalem3  24846  bposlem6  25059  uhgrvd00  26486  pthdlem2lem  26719  frcond2  27247  lnon0  27781  ocnel  28285  h1dn0  28539  cnlnssadj  29067  cvnbtwn2  29274  cvnbtwn3  29275  cvnbtwn4  29276  dmdbr2  29290  dmdbr3  29292  dmdbr4  29293  superpos  29341  atcvati  29373  mdsymlem4  29393  sumdmdii  29402  cdj3lem1  29421  elicoelioo  29668  archiabl  29880  bnj1280  31214  erdszelem9  31307  untangtr  31717  3orel2  31718  dfon2lem6  31817  dfon2lem7  31818  nofv  31935  sltres  31940  noetalem3  31990  outsideofrflx  32359  trer  32435  elicc3  32436  nn0prpw  32443  bj-cbvexdv  32861  bj-syl66ib  32958  bj-spcimdv  33009  bj-spcimdvv  33010  topdifinffinlem  33325  icorempt2  33329  isbasisrelowllem1  33333  relowlpssretop  33342  wl-mo3t  33488  poimirlem23  33562  poimirlem29  33568  poimirlem32  33571  poimir  33572  mblfinlem2  33577  sdclem1  33669  fdc  33671  incsequz  33674  rngosn3  33853  0rngo  33956  dmncan1  34005  bicomdd  34457  prtlem15  34479  lsatcvat  34655  lfl1  34675  hlrelat2  35007  cvrat  35026  linepsubN  35356  2llnma3r  35392  dihjatcclem4  37027  dochexmidlem1  37066  rngunsnply  38060  mptrcllem  38237  frege124d  38370  frege77  38551  frege116  38590  or3or  38636  clsk1indlem3  38658  ssralv2  39054  truniALT  39068  onfrALTlem3  39076  onfrALTlem2  39078  onfrALTlem1  39080  ax6e2ndeq  39092  stoweidlem62  40597  atbiffatnnb  41400  2reu3  41509  gbowge7  41976  gbege6  41978  copisnmnd  42134  setrec1lem4  42762
  Copyright terms: Public domain W3C validator