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

Theorem syl6bb 194
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 186 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl6rbb  195  syl6bbr  196  3bitr3g  220  bibi2i  225  ibibr  244  imanst  779  imandc  824  pm5.75  908  xordidc  1335  19.17  1493  alexdc  1555  nf4dc  1605  abeq2d  2200  cbvralf  2584  cbvrexf  2585  cbvreu  2588  cbvrab  2617  ceqsralt  2646  ralab2  2777  rexab2  2779  euxfr2dc  2798  reu7  2808  reu8  2809  cbvralcsf  2988  cbvrexcsf  2989  cbvreucsf  2990  cbvrabcsf  2991  ralss  3085  rexss  3086  prssg  3589  2ralunsn  3637  eluniab  3660  elintab  3694  dfiun2g  3757  dfiin2g  3758  cbvopab1  3903  cbvmpt  3925  axsep2  3950  bnd2  4000  opeqsn  4070  reusv3  4273  tfisi  4392  opeliunxp  4481  eliunxp  4563  relop  4574  eldm2g  4620  reldm0  4642  relrn0  4683  xpmlem  4839  elxp5  4906  cnvpom  4960  cbviota  4972  iota1  4981  sniota  4994  fncnv  5066  fnres  5116  brprcneu  5282  fnopfvb  5330  fvelrnb  5336  fvelimab  5344  fvopab3g  5361  eqfnfv3  5383  eqfnfv2f  5385  fvreseq  5387  fnreseql  5393  rexsupp  5407  respreima  5411  rexrn  5420  ralrn  5421  f1ompt  5434  fsn  5453  fconstfvm  5497  fconst3m  5498  fconst4m  5499  foima2  5512  rexima  5516  ralima  5517  dff13  5529  foeqcnvco  5551  fliftfun  5557  isocnv  5572  isoini  5579  f1oiso  5587  cbvriota  5600  eusvobj2  5620  oprabid  5663  eloprabga  5717  resoprab  5723  eqfnov  5733  eqfnov2  5734  ov6g  5764  funimassov  5776  ovelimab  5777  caovord2  5799  releldm2  5937  dfoprab4  5944  xporderlem  5978  poxp  5979  f1od2  5982  mpt2xopovel  5988  brtpos2  5998  brtpos0  5999  rntpos  6004  dftpos3  6009  tpostpos  6011  tpossym  6023  tposoprab  6027  tfrcllemres  6109  frecabcl  6146  frecsuclem  6153  erth2  6317  qliftfun  6354  erovlem  6364  ecopovsym  6368  ecopovsymg  6371  th3qlem1  6374  mapdm0  6400  elpmg  6401  elpm2g  6402  map0e  6423  dom2lem  6469  mapsnen  6508  xpdom2  6527  xpf1o  6540  mapen  6542  ssfilem  6571  diffitest  6583  ac6sfi  6594  isoti  6681  cnvti  6693  ltexpi  6875  ordpipqqs  6912  ltexnqq  6946  enq0enq  6969  enq0sym  6970  enq0tr  6972  nqnq0pi  6976  genipv  7047  genprndl  7059  genprndu  7060  genpdisj  7061  genpassl  7062  genpassu  7063  addcomprg  7116  mulcomprg  7118  ltnqpr  7131  ltnqpri  7132  ltexprlemm  7138  ltexprlemdisj  7144  ltsrprg  7272  mulgt0sr  7302  elreal2  7347  ltresr  7355  ltresr2  7356  axprecex  7394  axpre-ltadd  7400  axpre-mulgt0  7401  axpre-mulext  7402  subcan2  7686  negcon1  7713  negcon2  7714  lt0neg1  7925  lt0neg2  7926  le0neg1  7927  le0neg2  7928  reapirr  8030  reapmul1  8048  reapneg  8050  remulext1  8052  apti  8075  negap0  8082  divmulap2  8117  reclt1  8329  recgt1  8330  suprleubex  8387  addltmul  8622  elznn0  8735  zapne  8791  zltlen  8795  nn0lt10b  8797  nn0lt2  8798  eluz1  8992  raluz  9035  rexuz  9037  qltlen  9094  cnref1o  9102  rpnegap  9135  ltxr  9215  xlt0neg1  9269  xlt0neg2  9270  xle0neg1  9271  xle0neg2  9272  elixx1  9284  elixx3g  9288  elioo2  9308  icc0r  9313  elicc4  9327  elioopnf  9354  elioomnf  9355  iooneg  9374  iccneg  9375  iccshftr  9380  iccshftl  9382  iccdil  9384  icccntr  9386  iccf1o  9390  elfz1  9398  0fz1  9428  fzpr  9458  fzdifsuc  9462  uzsplit  9473  elfzm1b  9479  elfzp12  9480  fznn0  9494  exfzdc  9616  flqeqceilz  9690  zmodid2  9724  expap0  9950  bernneq  10039  hasheqf1o  10158  hashfacen  10206  sqrtmsq2i  10533  maxclpr  10620  minmax  10625  clim0  10637  climrecvg1n  10701  isummo  10737  fsumsplit  10764  dvdsval2  10881  odd2np1lem  10954  even2n  10956  divalgb  11007  divalgmod  11009  zsupcllemstep  11023  gcddvds  11037  bezoutlemmain  11069  isprm3  11182  prmind2  11184  dvdsprime  11186  coprm  11205  prmdvdsexp  11209  sqrt2irr  11223  sqpweven  11235  2sqpwodd  11236
  Copyright terms: Public domain W3C validator