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  706  con1biidc  770  pm4.54dc  804  dn1dc  866  dedlem0a  874  xorbi12d  1271  nbbndc  1282  eleq12d  2105  neeq12d  2220  neleq12d  2297  raleqbi1dv  2507  rexeqbi1dv  2508  reueqd  2509  rmoeqd  2510  raleqbidv  2511  rexeqbidv  2512  raleqbidva  2513  rexeqbidva  2514  eueq3dc  2709  sbc19.21g  2820  sbcabel  2833  sbcel1g  2863  sbceq1g  2864  sbcel2g  2865  sbceq2g  2866  sbccsb2g  2873  sbcco3g  2897  sseq12d  2968  psseq12d  3032  raaanlem  3320  sbcssg  3324  ralsng  3402  rexsng  3403  2ralunsn  3560  csbunig  3579  disjeq12d  3745  breq123d  3769  sbcbr12g  3805  sbcbr1g  3806  sbcbr2g  3807  treq  3851  nalset  3878  copsex4g  3975  sucelon  4195  posng  4355  csbxpg  4364  sbcrel  4369  csbcnvg  4462  eliniseg  4638  brcodir  4655  csbrng  4725  sbcfung  4868  fneq12d  4934  feq12d  4979  feq123d  4980  sbcfng  4987  sbcfg  4988  f1osng  5110  csbfv12g  5152  funimass4  5167  dmfco  5184  eqfnfv  5208  eqfnfv2  5209  fneqeql2  5219  fvimacnvi  5224  funimass3  5226  fniniseg  5230  rexsupp  5234  unpreima  5235  ralrnmpt  5252  rexrnmpt  5253  dffo3  5257  fmptco  5273  fressnfv  5293  eufnfv  5332  fnunirn  5349  dff13  5350  f1elima  5355  cocan1  5370  cocan2  5371  fliftel  5376  fliftf  5382  isoresbr  5392  isoini  5400  f1oiso  5408  f1ofveu  5443  mpt2eq123dva  5508  ovid  5559  ov  5562  ovg  5581  ovelrn  5591  caovord2d  5612  ofrfval2  5669  offveqb  5672  eqop  5745  reldm  5754  mpt2xopoveq  5796  mpt2xopovel  5797  isprmpt2  5799  tpostpos  5820  smoiso  5858  frecsuclem3  5929  nnaordr  6019  nnaword  6020  nnaordex  6036  ereq1  6049  brdifun  6069  erth2  6087  qliftfun  6124  brecop  6132  dom2lem  6188  xpcomco  6236  ltapig  6322  ltmpig  6323  nlt1pig  6325  mulcmpblnq  6352  ltsonq  6382  lt2addnq  6388  archnqq  6400  prarloclemarch  6401  ltrnqg  6403  mulcmpblnq0  6427  preqlu  6455  genpdflem  6490  addnqprllem  6510  addnqprulem  6511  addlocprlemgt  6517  appdivnq  6544  mulnqprl  6549  mulnqpru  6550  mullocprlem  6551  distrlem4prl  6560  distrlem4pru  6561  1idprl  6566  1idpru  6567  ltexprlemloc  6581  cauappcvgprlemladdrl  6629  cauappcvgprlemladd  6630  cauappcvgprlem1  6631  archrecnq  6635  caucvgprlemnkj  6637  addcmpblnr  6667  lttrsr  6690  ltsosr  6692  ltasrg  6698  mulextsr1  6707  ltresr  6736  cnegexlem1  6983  negeu  6999  subadd2  7012  subcan2  7032  ltadd1  7219  leadd2  7221  ltsubadd  7222  lesubadd  7224  ltaddsub2  7227  leaddsub2  7229  ltaddpos  7242  lesub2  7247  ltsub2  7249  ltnegcon1  7253  ltnegcon2  7254  lenegcon1  7256  lenegcon2  7257  addge01  7262  addge02  7263  suble0  7266  leaddle0  7267  lesub0  7269  recexre  7362  reaplt  7372  reapltxor  7373  reapneg  7381  remulext1  7383  apreim  7387  apcotr  7391  apadd2  7393  addext  7394  mulcanap2d  7425  diveqap0  7443  diveqap1  7464  ltmul2  7603  lemul2  7604  ltmulgt11  7611  ltmulgt12  7612  gt0div  7617  ge0div  7618  ltmuldiv  7621  ltrec1  7635  lerec2  7636  ledivdiv  7637  ltdiv23  7639  lediv23  7640  creur  7692  creui  7693  nn1suc  7714  nnrecl  7955  znnsub  8072  zgt0ge1  8078  zltlen  8095  nn0n0n1ge2b  8096  btwnnz  8110  gtndiv  8111  prime  8113  eluz2  8255  indstr2  8322  negm  8326  nn01to3  8328  qapne  8350  qreccl  8351  iccid  8564  elioc2  8575  elico2  8576  elicc2  8577  elfz2  8651  fzen  8677  fzsubel  8693  elfzp1  8704  fzpr  8709  fzrevral2  8738  fzrevral3  8739  nn0disj  8765  2ffzeq  8768  fzosplitsni  8861  frecuzrdgfn  8879  nn0ennn  8890  sq11  8979  cjap  9134  cbvrald  9262  bj-nalset  9350  bj-sels  9369  bj-nnelirr  9413
  Copyright terms: Public domain W3C validator