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  6436  ltmpig  6437  nlt1pig  6439  mulcmpblnq  6466  ltsonq  6496  lt2addnq  6502  lt2mulnq  6503  archnqq  6515  prarloclemarch  6516  ltrnqg  6518  mulcmpblnq0  6542  preqlu  6570  genpdflem  6605  addnqprllem  6625  addnqprulem  6626  addlocprlemgt  6632  appdivnq  6661  mulnqprl  6666  mulnqpru  6667  mullocprlem  6668  distrlem4prl  6682  distrlem4pru  6683  1idprl  6688  1idpru  6689  ltexprlemloc  6705  cauappcvgprlemladdrl  6755  cauappcvgprlemladd  6756  cauappcvgprlem1  6757  archrecnq  6761  caucvgprlemnkj  6764  caucvgprprlemexb  6805  addcmpblnr  6824  lttrsr  6847  ltsosr  6849  ltasrg  6855  mulextsr1  6865  srpospr  6867  caucvgsrlemcau  6877  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  ltresr  6915  axcaucvglemres  6973  cnegexlem1  7186  negeu  7202  subadd2  7215  subcan2  7236  ltadd1  7424  leadd2  7426  ltsubadd  7427  lesubadd  7429  ltaddsub2  7432  leaddsub2  7434  ltaddpos  7447  lesub2  7452  ltsub2  7454  ltnegcon1  7458  ltnegcon2  7459  lenegcon1  7461  lenegcon2  7462  addge01  7467  addge02  7468  suble0  7471  leaddle0  7472  lesub0  7474  sublt0d  7561  recexre  7569  reaplt  7579  reapltxor  7580  reapneg  7588  remulext1  7590  apreim  7594  apcotr  7598  apadd2  7600  addext  7601  mulcanap2d  7643  diveqap0  7661  diveqap1  7682  ltmul2  7822  lemul2  7823  ltmulgt11  7830  ltmulgt12  7831  gt0div  7836  ge0div  7837  ltmuldiv  7840  ltrec1  7854  lerec2  7855  ledivdiv  7856  ltdiv23  7858  lediv23  7859  creur  7911  creui  7912  nn1suc  7933  nnrecl  8179  znnsub  8296  zgt0ge1  8302  zltlen  8319  nn0n0n1ge2b  8320  btwnnz  8334  gtndiv  8335  prime  8337  eluz2  8479  indstr2  8546  negm  8550  nn01to3  8552  qapne  8574  qltlen  8575  qreccl  8576  divlt1lt  8650  divle1le  8651  iccid  8794  elioc2  8805  elico2  8806  elicc2  8807  elfz2  8881  fzen  8907  fzsubel  8923  elfzp1  8934  fzpr  8939  fzrevral2  8968  fzrevral3  8969  nn0disj  8995  2ffzeq  8998  fzosplitsni  9091  fvinim0ffz  9096  modq0  9171  negqmod0  9173  frecuzrdgfn  9198  nn0ennn  9209  sq11  9326  2shfti  9432  cjap  9506  rexanuz2  9589  abs00ap  9660  absext  9661  sqabs  9678  abslt  9684  absle  9685  absdiflt  9688  absdifle  9689  lenegsq  9691  clim  9802  clim0c  9807  climrecvg1n  9867  nn0seqcvgd  9880  algcvgblem  9888  cbvrald  9927  bj-nalset  10015  bj-sels  10034  bj-nnelirr  10078
  Copyright terms: Public domain W3C validator