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  imandc  820  pm5.75  904  xordidc  1331  19.17  1489  alexdc  1551  nf4dc  1601  abeq2d  2192  cbvralf  2572  cbvrexf  2573  cbvreu  2576  cbvrab  2600  ceqsralt  2627  ralab2  2757  rexab2  2759  euxfr2dc  2778  reu7  2788  reu8  2789  cbvralcsf  2965  cbvrexcsf  2966  cbvreucsf  2967  cbvrabcsf  2968  ralss  3061  rexss  3062  prssg  3550  2ralunsn  3598  eluniab  3621  elintab  3655  dfiun2g  3718  dfiin2g  3719  cbvopab1  3859  cbvmpt  3880  axsep2  3905  bnd2  3955  opeqsn  4015  reusv3  4218  tfisi  4336  opeliunxp  4421  eliunxp  4503  relop  4514  eldm2g  4559  reldm0  4581  relrn0  4622  xpmlem  4774  elxp5  4839  cnvpom  4890  cbviota  4902  iota1  4911  sniota  4924  fncnv  4996  fnres  5046  brprcneu  5202  fnopfvb  5247  fvelrnb  5253  fvelimab  5261  fvopab3g  5277  eqfnfv3  5299  eqfnfv2f  5301  fvreseq  5303  fnreseql  5309  rexsupp  5323  respreima  5327  rexrn  5336  ralrn  5337  f1ompt  5352  fsn  5367  fconstfvm  5411  fconst3m  5412  fconst4m  5413  rexima  5426  ralima  5427  dff13  5439  foeqcnvco  5461  fliftfun  5467  isocnv  5482  isoini  5488  f1oiso  5496  cbvriota  5509  eusvobj2  5529  oprabid  5568  eloprabga  5622  resoprab  5628  eqfnov  5638  eqfnov2  5639  ov6g  5669  funimassov  5681  ovelimab  5682  caovord2  5704  releldm2  5842  dfoprab4  5849  xporderlem  5883  poxp  5884  f1od2  5887  mpt2xopovel  5890  brtpos2  5900  brtpos0  5901  rntpos  5906  dftpos3  5911  tpostpos  5913  tpossym  5925  tposoprab  5929  tfrcllemres  6011  frecabcl  6048  frecsuclem  6055  erth2  6217  qliftfun  6254  erovlem  6264  ecopovsym  6268  ecopovsymg  6271  th3qlem1  6274  dom2lem  6319  xpdom2  6375  xpf1o  6385  ssfilem  6410  diffitest  6421  ac6sfi  6431  isoti  6479  cnvti  6491  ltexpi  6589  ordpipqqs  6626  ltexnqq  6660  enq0enq  6683  enq0sym  6684  enq0tr  6686  nqnq0pi  6690  genipv  6761  genprndl  6773  genprndu  6774  genpdisj  6775  genpassl  6776  genpassu  6777  addcomprg  6830  mulcomprg  6832  ltnqpr  6845  ltnqpri  6846  ltexprlemm  6852  ltexprlemdisj  6858  ltsrprg  6986  mulgt0sr  7016  elreal2  7061  ltresr  7069  ltresr2  7070  axprecex  7108  axpre-ltadd  7114  axpre-mulgt0  7115  axpre-mulext  7116  subcan2  7400  negcon1  7427  negcon2  7428  lt0neg1  7639  lt0neg2  7640  le0neg1  7641  le0neg2  7642  reapirr  7744  reapmul1  7762  reapneg  7764  remulext1  7766  apti  7789  negap0  7796  divmulap2  7831  reclt1  8041  recgt1  8042  suprleubex  8099  addltmul  8334  elznn0  8447  zapne  8503  zltlen  8507  nn0lt10b  8509  nn0lt2  8510  eluz1  8704  raluz  8747  rexuz  8749  qltlen  8806  cnref1o  8814  rpnegap  8847  ltxr  8927  xlt0neg1  8981  xlt0neg2  8982  xle0neg1  8983  xle0neg2  8984  elixx1  8996  elixx3g  9000  elioo2  9020  icc0r  9025  elicc4  9039  elioopnf  9066  elioomnf  9067  iooneg  9086  iccneg  9087  iccshftr  9092  iccshftl  9094  iccdil  9096  icccntr  9098  iccf1o  9102  elfz1  9110  0fz1  9140  fzpr  9170  fzdifsuc  9174  uzsplit  9185  elfzm1b  9191  elfzp12  9192  fznn0  9206  exfzdc  9326  flqeqceilz  9400  zmodid2  9434  expap0  9603  bernneq  9690  sizeeqf1o  9809  sqrtmsq2i  10159  maxclpr  10246  minmax  10250  clim0  10262  climrecvg1n  10323  dvdsval2  10343  odd2np1lem  10416  even2n  10418  divalgb  10469  divalgmod  10471  zsupcllemstep  10485  gcddvds  10499  bezoutlemmain  10531  isprm3  10644  prmind2  10646  dvdsprime  10648  coprm  10667  prmdvdsexp  10671  sqrt2irr  10685  sqpweven  10697  2sqpwodd  10698
  Copyright terms: Public domain W3C validator