ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bitrd Structured version   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  691  con1biidc  755  pm4.54dc  789  dn1dc  851  dedlem0a  859  xorbi12d  1255  nbbndc  1266  eleq12d  2084  neeq12d  2198  neleq12d  2275  raleqbi1dv  2485  rexeqbi1dv  2486  reueqd  2487  rmoeqd  2488  raleqbidv  2489  rexeqbidv  2490  raleqbidva  2491  rexeqbidva  2492  eueq3dc  2686  sbc19.21g  2797  sbcabel  2810  sbcel1g  2840  sbceq1g  2841  sbcel2g  2842  sbceq2g  2843  sbccsb2g  2850  sbcco3g  2874  sseq12d  2945  psseq12d  3009  raaanlem  3297  sbcssg  3301  ralsng  3377  rexsng  3378  2ralunsn  3535  csbunig  3554  disjeq12d  3720  breq123d  3744  sbcbr12g  3780  sbcbr1g  3781  sbcbr2g  3782  treq  3826  nalset  3853  copsex4g  3950  sucelon  4170  posng  4330  csbxpg  4339  sbcrel  4344  csbcnvg  4437  eliniseg  4613  brcodir  4630  csbrng  4700  sbcfung  4842  fneq12d  4908  feq12d  4953  feq123d  4954  sbcfng  4961  sbcfg  4962  f1osng  5083  csbfv12g  5125  funimass4  5140  dmfco  5157  eqfnfv  5181  eqfnfv2  5182  fneqeql2  5192  fvimacnvi  5197  funimass3  5199  fniniseg  5203  rexsupp  5207  unpreima  5208  ralrnmpt  5225  rexrnmpt  5226  dffo3  5230  fmptco  5246  fressnfv  5266  eufnfv  5305  fnunirn  5322  dff13  5323  f1elima  5328  cocan1  5343  cocan2  5344  fliftel  5349  fliftf  5355  isoresbr  5365  isoini  5373  f1oiso  5381  f1ofveu  5415  mpt2eq123dva  5480  ovid  5531  ov  5534  ovg  5553  ovelrn  5563  caovord2d  5584  ofrfval2  5641  offveqb  5644  eqop  5717  reldm  5726  mpt2xopoveq  5768  mpt2xopovel  5769  isprmpt2  5771  tpostpos  5792  smoiso  5830  frecsuclem3  5897  nnaordr  5985  nnaword  5986  nnaordex  6002  ereq1  6015  brdifun  6035  erth2  6053  qliftfun  6090  brecop  6098  ltapig  6187  ltmpig  6188  nlt1pig  6190  mulcmpblnq  6216  ltsonq  6246  lt2addnq  6252  archnqq  6263  prarloclemarch  6264  ltrnqg  6266  mulcmpblnq0  6288  preqlu  6315  genpdflem  6350  addnqprllem  6371  addnqprulem  6372  addlocprlemgt  6378  appdivnq  6396  mulnqprl  6401  mulnqpru  6402  mullocprlem  6403  distrlem4prl  6412  distrlem4pru  6413  1idprl  6418  1idpru  6419  ltexprlemloc  6433  addcmpblnr  6480  lttrsr  6503  ltsosr  6505  ltasrg  6511  mulextsr1  6520  ltresr  6548  cnegexlem1  6789  negeu  6805  subadd2  6818  subcan2  6838  ltadd1  7025  leadd2  7027  ltsubadd  7028  lesubadd  7030  ltaddsub2  7033  leaddsub2  7035  ltaddpos  7048  lesub2  7053  ltsub2  7055  ltnegcon1  7059  ltnegcon2  7060  lenegcon1  7062  lenegcon2  7063  addge01  7068  addge02  7069  suble0  7072  leaddle0  7073  lesub0  7075  recexre  7168  reaplt  7178  reapltxor  7179  reapneg  7187  remulext1  7189  apreim  7193  apcotr  7197  apadd2  7199  addext  7200  mulcanap2d  7231  diveqap0  7249  diveqap1  7270  ltmul2  7408  lemul2  7409  ltmulgt11  7416  ltmulgt12  7417  gt0div  7422  ge0div  7423  ltmuldiv  7426  ltrec1  7440  lerec2  7441  ledivdiv  7442  ltdiv23  7444  lediv23  7445  creur  7497  creui  7498  nn1suc  7519  znnsub  7870  zgt0ge1  7876  zltlen  7888  btwnnz  7902  gtndiv  7903  prime  7905  qapne  8060  qreccl  8061  iccid  8273  elioc2  8284  elico2  8285  elicc2  8286  cbvrald  8384  bj-nalset  8468  bj-sels  8487  bj-nnelirr  8529
  Copyright terms: Public domain W3C validator