ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6bb GIF version

Theorem syl6bb 185
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 9 . 2 (𝜑 → (𝜒𝜃))
41, 3bitrd 177 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl6rbb  186  syl6bbr  187  3bitr3g  211  bibi2i  216  ibibr  235  imandc  786  pm5.75  869  xordidc  1290  19.17  1448  alexdc  1510  nf4dc  1560  abeq2d  2150  cbvralf  2527  cbvrexf  2528  cbvreu  2531  cbvrab  2555  ceqsralt  2581  ralab2  2705  rexab2  2707  euxfr2dc  2726  reu7  2736  reu8  2737  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  ralss  3006  rexss  3007  prssg  3521  2ralunsn  3569  eluniab  3592  elintab  3626  dfiun2g  3689  dfiin2g  3690  cbvopab1  3830  cbvmpt  3851  axsep2  3876  bnd2  3926  opeqsn  3989  reusv3  4192  tfisi  4310  opeliunxp  4395  eliunxp  4475  relop  4486  eldm2g  4531  reldm0  4553  relrn0  4594  xpmlem  4744  elxp5  4809  cnvpom  4860  cbviota  4872  iota1  4881  sniota  4894  fncnv  4965  fnres  5015  brprcneu  5171  fnopfvb  5215  fvelrnb  5221  fvelimab  5229  fvopab3g  5245  eqfnfv3  5267  eqfnfv2f  5269  fvreseq  5271  fnreseql  5277  rexsupp  5291  respreima  5295  rexrn  5304  ralrn  5305  f1ompt  5320  fsn  5335  fconstfvm  5379  fconst3m  5380  fconst4m  5381  rexima  5394  ralima  5395  dff13  5407  foeqcnvco  5430  fliftfun  5436  isocnv  5451  isoini  5457  f1oiso  5465  cbvriota  5478  eusvobj2  5498  oprabid  5537  eloprabga  5591  resoprab  5597  eqfnov  5607  eqfnov2  5608  ov6g  5638  funimassov  5650  ovelimab  5651  caovord2  5673  releldm2  5811  dfoprab4  5818  xporderlem  5852  poxp  5853  mpt2xopovel  5856  brtpos2  5866  brtpos0  5867  rntpos  5872  dftpos3  5877  tpostpos  5879  tpossym  5891  tposoprab  5895  frecsuclem3  5990  erth2  6151  qliftfun  6188  erovlem  6198  ecopovsym  6202  ecopovsymg  6205  th3qlem1  6208  dom2lem  6252  xpdom2  6305  ssfiexmid  6336  diffitest  6344  ac6sfi  6352  ltexpi  6435  ordpipqqs  6472  ltexnqq  6506  enq0enq  6529  enq0sym  6530  enq0tr  6532  nqnq0pi  6536  genipv  6607  genprndl  6619  genprndu  6620  genpdisj  6621  genpassl  6622  genpassu  6623  addcomprg  6676  mulcomprg  6678  ltnqpr  6691  ltnqpri  6692  ltexprlemm  6698  ltexprlemdisj  6704  ltsrprg  6832  mulgt0sr  6862  elreal2  6907  ltresr  6915  ltresr2  6916  axprecex  6954  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  subcan2  7236  negcon1  7263  negcon2  7264  lt0neg1  7463  lt0neg2  7464  le0neg1  7465  le0neg2  7466  reapirr  7568  reapmul1  7586  reapneg  7588  remulext1  7590  apti  7613  negap0  7620  divmulap2  7655  reclt1  7862  recgt1  7863  addltmul  8161  elznn0  8260  zapne  8315  zltlen  8319  nn0lt10b  8321  nn0lt2  8322  eluz1  8477  raluz  8521  rexuz  8523  qltlen  8575  cnref1o  8582  rpnegap  8615  ltxr  8695  xlt0neg1  8751  xlt0neg2  8752  xle0neg1  8753  xle0neg2  8754  elixx1  8766  elixx3g  8770  elioo2  8790  icc0r  8795  elicc4  8809  elioopnf  8836  elioomnf  8837  iooneg  8856  iccneg  8857  iccshftr  8862  iccshftl  8864  iccdil  8866  icccntr  8868  iccf1o  8872  elfz1  8879  0fz1  8909  fzpr  8939  fzdifsuc  8943  uzsplit  8954  elfzm1b  8960  elfzp12  8961  fznn0  8974  flqeqceilz  9160  expap0  9285  bernneq  9369  sqrtmsq2i  9731  clim0  9806  climrecvg1n  9867  sqrt2irr  9878
  Copyright terms: Public domain W3C validator