NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl6bb GIF version

Theorem syl6bb 252
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6bb.1 (φ → (ψχ))
syl6bb.2 (χθ)
Assertion
Ref Expression
syl6bb (φ → (ψθ))

Proof of Theorem syl6bb
StepHypRef Expression
1 syl6bb.1 . 2 (φ → (ψχ))
2 syl6bb.2 . . 3 (χθ)
32a1i 10 . 2 (φ → (χθ))
41, 3bitrd 244 1 (φ → (ψθ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176
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 177
This theorem is referenced by:  syl6rbb  253  syl6bbr  254  3bitr3g  278  bibi2i  304  ibibr  332  pm5.75  903  cadan  1392  19.17  1861  2eu6  2289  abeq2d  2462  necon2bbid  2574  cbvralf  2829  cbvreu  2833  cbvrab  2857  ceqsralt  2882  ralab2  3001  rexab2  3003  reu7  3031  reu8  3032  2reu5  3044  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  elcomplg  3218  ralss  3332  rexss  3333  prssg  3862  ssunsn2  3865  eqsn  3867  2ralunsn  3880  eluniab  3903  elintab  3937  dfiun2g  3999  dfiin2g  4000  elpw1  4144  eqpw1  4162  pw1in  4164  pw1disj  4167  eluni1g  4172  ssrelk  4211  eqrelk  4212  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  elimakvg  4258  opkelcokg  4261  elp6  4263  opkelimagekg  4271  dfimak2  4298  eqpw1uni  4330  cbviota  4344  iota1  4353  sniota  4369  dfnnc2  4395  nnsucelr  4428  nndisjeq  4429  ltfinex  4464  ltfintri  4466  ssfin  4470  ncfinlower  4483  evenodddisj  4516  nnadjoin  4520  nnpweq  4523  sfindbl  4530  sfintfin  4532  tfinnn  4534  dfphi2  4569  0cnelphi  4597  proj1op  4600  cbvopab1  4632  setconslem6  4736  opeliunxp  4820  eliunxp  4821  brswap2  4860  elres  4995  xpcan  5057  xpcan2  5058  fncnv  5158  fnres  5199  fun11iun  5305  fnopfvb  5359  funopfvb  5361  fvelrnb  5365  funimass4  5368  fvopab3g  5386  eqfnfv3  5394  eqfnfv2f  5396  fvreseq  5398  inpreima  5409  respreima  5410  fnasrn  5417  fsn  5432  fconstfv  5456  dff13  5471  isocnv  5491  isoini  5497  f1oiso  5499  xpnedisj  5513  funsi  5520  oprabid  5550  eloprabga  5578  resoprab  5581  eqfnov  5589  eqfnov2  5590  ov6g  5600  ovelrn  5608  funimassov  5609  ovelimab  5610  ndmovg  5613  caovord2  5630  cbvmpt  5676  brsnsi  5773  brimage  5793  fntxp  5804  addcfnex  5824  brpprod  5839  fnpprod  5843  pw1fnf1o  5855  clos1ex  5876  erth2  5969  elpmg  6013  elpm2g  6014  xpassenlem  6056  enpw1  6062  enmap2lem3  6065  enprmaplem3  6078  peano4nc  6150  ncspw1eu  6159  ce0addcnnul  6179  nc0suc  6217  taddc  6229  ce0lenc1  6239  muc0or  6252  csucex  6259  addccan2nclem1  6263  nnc3n3p1  6278  nchoicelem12  6300  nchoicelem17  6305  frecxp  6314  fnfreclem3  6319  fnfrec  6320  frecsuc  6322  scancan  6331
  Copyright terms: Public domain W3C validator