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  6433  ordpipqqs  6470  ltexnqq  6504  enq0enq  6527  enq0sym  6528  enq0tr  6530  nqnq0pi  6534  genipv  6605  genprndl  6617  genprndu  6618  genpdisj  6619  genpassl  6620  genpassu  6621  addcomprg  6674  mulcomprg  6676  ltnqpr  6689  ltnqpri  6690  ltexprlemm  6696  ltexprlemdisj  6702  ltsrprg  6830  mulgt0sr  6860  elreal2  6905  ltresr  6913  ltresr2  6914  axprecex  6952  axpre-ltadd  6958  axpre-mulgt0  6959  axpre-mulext  6960  subcan2  7234  negcon1  7261  negcon2  7262  lt0neg1  7461  lt0neg2  7462  le0neg1  7463  le0neg2  7464  reapirr  7566  reapmul1  7584  reapneg  7586  remulext1  7588  apti  7611  negap0  7618  divmulap2  7653  reclt1  7860  recgt1  7861  addltmul  8159  elznn0  8258  zapne  8313  zltlen  8317  nn0lt10b  8319  nn0lt2  8320  eluz1  8475  raluz  8519  rexuz  8521  qltlen  8573  cnref1o  8580  rpnegap  8613  ltxr  8693  xlt0neg1  8749  xlt0neg2  8750  xle0neg1  8751  xle0neg2  8752  elixx1  8764  elixx3g  8768  elioo2  8788  icc0r  8793  elicc4  8807  elioopnf  8834  elioomnf  8835  iooneg  8854  iccneg  8855  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  iccf1o  8870  elfz1  8877  0fz1  8907  fzpr  8937  fzdifsuc  8941  uzsplit  8952  elfzm1b  8958  elfzp12  8959  fznn0  8972  flqeqceilz  9158  expap0  9259  bernneq  9343  sqrtmsq2i  9705  clim0  9780  climrecvg1n  9841  sqrt2irr  9852
  Copyright terms: Public domain W3C validator