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

Theorem bitrd 177
Description: Deduction form of bitri 173. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)
Hypotheses
Ref Expression
bitrd.1 (𝜑 → (𝜓𝜒))
bitrd.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
bitrd (𝜑 → (𝜓𝜃))

Proof of Theorem bitrd
StepHypRef Expression
1 bitrd.1 . . . 4 (𝜑 → (𝜓𝜒))
21pm5.74i 169 . . 3 ((𝜑𝜓) ↔ (𝜑𝜒))
3 bitrd.2 . . . 4 (𝜑 → (𝜒𝜃))
43pm5.74i 169 . . 3 ((𝜑𝜒) ↔ (𝜑𝜃))
52, 4bitri 173 . 2 ((𝜑𝜓) ↔ (𝜑𝜃))
65pm5.74ri 170 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:  bitr2d  178  bitr3d  179  bitr4d  180  syl5bb  181  syl6bb  185  3bitrd  203  3bitr2d  205  3bitr3d  207  3bitr4d  209  imbi12d  223  bibi12d  224  sylan9bb  435  anbi12d  442  orbi12d  707  con1biidc  771  pm4.54dc  805  dn1dc  867  dedlem0a  875  xorbi12d  1273  nbbndc  1285  eleq12d  2108  neeq12d  2225  neleq12d  2303  raleqbi1dv  2513  rexeqbi1dv  2514  reueqd  2515  rmoeqd  2516  raleqbidv  2517  rexeqbidv  2518  raleqbidva  2519  rexeqbidva  2520  eueq3dc  2715  sbc19.21g  2826  sbcabel  2839  sbcel1g  2869  sbceq1g  2870  sbcel2g  2871  sbceq2g  2872  sbccsb2g  2879  sbcco3g  2903  sseq12d  2974  psseq12d  3038  raaanlem  3326  sbcssg  3330  ralsng  3411  rexsng  3412  2ralunsn  3569  csbunig  3588  disjeq12d  3754  breq123d  3778  sbcbr12g  3814  sbcbr1g  3815  sbcbr2g  3816  treq  3860  nalset  3887  copsex4g  3984  sucelon  4229  posng  4412  csbxpg  4421  sbcrel  4426  csbcnvg  4519  eliniseg  4695  brcodir  4712  csbrng  4782  sbcfung  4925  fneq12d  4991  feq12d  5036  feq123d  5037  sbcfng  5044  sbcfg  5045  f1osng  5167  csbfv12g  5209  funimass4  5224  dmfco  5241  eqfnfv  5265  eqfnfv2  5266  fneqeql2  5276  fvimacnvi  5281  funimass3  5283  fniniseg  5287  rexsupp  5291  unpreima  5292  ralrnmpt  5309  rexrnmpt  5310  dffo3  5314  fmptco  5330  fressnfv  5350  eufnfv  5389  fnunirn  5406  dff13  5407  f1elima  5412  cocan1  5427  cocan2  5428  fliftel  5433  fliftf  5439  isoresbr  5449  isoini  5457  f1oiso  5465  f1ofveu  5500  mpt2eq123dva  5566  ovid  5617  ov  5620  ovg  5639  ovelrn  5649  caovord2d  5670  ofrfval2  5727  offveqb  5730  eqop  5803  reldm  5812  mpt2xopoveq  5855  mpt2xopovel  5856  isprmpt2  5858  tpostpos  5879  smoiso  5917  frecsuclem3  5990  nnaordr  6083  nnaword  6084  nnaordex  6100  ereq1  6113  brdifun  6133  erth2  6151  qliftfun  6188  brecop  6196  dom2lem  6252  xpcomco  6300  php5fin  6339  ltapig  6434  ltmpig  6435  nlt1pig  6437  mulcmpblnq  6464  ltsonq  6494  lt2addnq  6500  lt2mulnq  6501  archnqq  6513  prarloclemarch  6514  ltrnqg  6516  mulcmpblnq0  6540  preqlu  6568  genpdflem  6603  addnqprllem  6623  addnqprulem  6624  addlocprlemgt  6630  appdivnq  6659  mulnqprl  6664  mulnqpru  6665  mullocprlem  6666  distrlem4prl  6680  distrlem4pru  6681  1idprl  6686  1idpru  6687  ltexprlemloc  6703  cauappcvgprlemladdrl  6753  cauappcvgprlemladd  6754  cauappcvgprlem1  6755  archrecnq  6759  caucvgprlemnkj  6762  caucvgprprlemexb  6803  addcmpblnr  6822  lttrsr  6845  ltsosr  6847  ltasrg  6853  mulextsr1  6863  srpospr  6865  caucvgsrlemcau  6875  caucvgsrlemgt1  6877  caucvgsrlemoffres  6882  ltresr  6913  axcaucvglemres  6971  cnegexlem1  7184  negeu  7200  subadd2  7213  subcan2  7234  ltadd1  7422  leadd2  7424  ltsubadd  7425  lesubadd  7427  ltaddsub2  7430  leaddsub2  7432  ltaddpos  7445  lesub2  7450  ltsub2  7452  ltnegcon1  7456  ltnegcon2  7457  lenegcon1  7459  lenegcon2  7460  addge01  7465  addge02  7466  suble0  7469  leaddle0  7470  lesub0  7472  sublt0d  7559  recexre  7567  reaplt  7577  reapltxor  7578  reapneg  7586  remulext1  7588  apreim  7592  apcotr  7596  apadd2  7598  addext  7599  mulcanap2d  7641  diveqap0  7659  diveqap1  7680  ltmul2  7820  lemul2  7821  ltmulgt11  7828  ltmulgt12  7829  gt0div  7834  ge0div  7835  ltmuldiv  7838  ltrec1  7852  lerec2  7853  ledivdiv  7854  ltdiv23  7856  lediv23  7857  creur  7909  creui  7910  nn1suc  7931  nnrecl  8177  znnsub  8294  zgt0ge1  8300  zltlen  8317  nn0n0n1ge2b  8318  btwnnz  8332  gtndiv  8333  prime  8335  eluz2  8477  indstr2  8544  negm  8548  nn01to3  8550  qapne  8572  qltlen  8573  qreccl  8574  divlt1lt  8648  divle1le  8649  iccid  8792  elioc2  8803  elico2  8804  elicc2  8805  elfz2  8879  fzen  8905  fzsubel  8921  elfzp1  8932  fzpr  8937  fzrevral2  8966  fzrevral3  8967  nn0disj  8993  2ffzeq  8996  fzosplitsni  9089  fvinim0ffz  9094  frecuzrdgfn  9172  nn0ennn  9183  sq11  9300  2shfti  9406  cjap  9480  rexanuz2  9563  abs00ap  9634  absext  9635  sqabs  9652  abslt  9658  absle  9659  absdiflt  9662  absdifle  9663  lenegsq  9665  clim  9775  clim0c  9780  climrecvg1n  9840  nn0seqcvgd  9853  algcvgblem  9861  cbvrald  9900  bj-nalset  9988  bj-sels  10007  bj-nnelirr  10051
  Copyright terms: Public domain W3C validator