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  438  anbi12d  445  orbi12d  694  con1biidc  764  pm4.54dc  798  dn1dc  855  dedlem0a  863  xorbi12d  1257  nbbndc  1268  eleq12d  2090  neeq12d  2204  neleq12d  2281  raleqbi1dv  2491  rexeqbi1dv  2492  reueqd  2493  rmoeqd  2494  raleqbidv  2495  rexeqbidv  2496  raleqbidva  2497  rexeqbidva  2498  eueq3dc  2692  sbc19.21g  2803  sbcabel  2816  sbcel1g  2846  sbceq1g  2847  sbcel2g  2848  sbceq2g  2849  sbccsb2g  2856  sbcco3g  2880  sseq12d  2951  psseq12d  3015  raaanlem  3305  sbcssg  3309  ralsng  3385  rexsng  3386  2ralunsn  3543  csbunig  3562  disjeq12d  3728  breq123d  3752  sbcbr12g  3788  sbcbr1g  3789  sbcbr2g  3790  treq  3834  nalset  3861  copsex4g  3958  sucelon  4179  posng  4339  csbxpg  4348  sbcrel  4353  csbcnvg  4446  eliniseg  4622  brcodir  4639  csbrng  4709  sbcfung  4851  fneq12d  4917  feq12d  4962  feq123d  4963  sbcfng  4970  sbcfg  4971  f1osng  5092  csbfv12g  5134  funimass4  5149  dmfco  5166  eqfnfv  5190  eqfnfv2  5191  fneqeql2  5201  fvimacnvi  5206  funimass3  5208  fniniseg  5212  rexsupp  5216  unpreima  5217  ralrnmpt  5234  rexrnmpt  5235  dffo3  5239  fmptco  5255  fressnfv  5275  eufnfv  5314  fnunirn  5331  dff13  5332  f1elima  5337  cocan1  5352  cocan2  5353  fliftel  5358  fliftf  5364  isoresbr  5374  isoini  5382  f1oiso  5390  f1ofveu  5424  mpt2eq123dva  5489  ovid  5540  ov  5543  ovg  5562  ovelrn  5572  caovord2d  5593  ofrfval2  5650  offveqb  5653  eqop  5726  reldm  5735  mpt2xopoveq  5777  mpt2xopovel  5778  isprmpt2  5780  tpostpos  5801  smoiso  5839  frecsuclem3  5906  nnaordr  5994  nnaword  5995  nnaordex  6011  ereq1  6024  brdifun  6044  erth2  6062  qliftfun  6099  brecop  6107  ltapig  6198  ltmpig  6199  nlt1pig  6201  mulcmpblnq  6227  ltsonq  6257  lt2addnq  6263  archnqq  6274  prarloclemarch  6275  ltrnqg  6277  mulcmpblnq0  6299  preqlu  6326  genpdflem  6361  addnqprllem  6382  addnqprulem  6383  addlocprlemgt  6389  appdivnq  6407  mulnqprl  6412  mulnqpru  6413  mullocprlem  6414  distrlem4prl  6423  distrlem4pru  6424  1idprl  6429  1idpru  6430  ltexprlemloc  6444  addcmpblnr  6486  lttrsr  6509  ltsosr  6511  ltasrg  6517  ltresr  6550  cnegexlem1  6773  negeu  6789  subadd2  6802  subcan2  6822  cbvrald  7034  bj-nalset  7118  bj-sels  7137  bj-nnelirr  7175
  Copyright terms: Public domain W3C validator