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  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  6426  preqlu  6454  genpdflem  6489  addnqprllem  6510  addnqprulem  6511  addlocprlemgt  6517  appdivnq  6542  mulnqprl  6547  mulnqpru  6548  mullocprlem  6549  distrlem4prl  6558  distrlem4pru  6559  1idprl  6564  1idpru  6565  ltexprlemloc  6579  addcmpblnr  6627  lttrsr  6650  ltsosr  6652  ltasrg  6658  mulextsr1  6667  ltresr  6696  cnegexlem1  6943  negeu  6959  subadd2  6972  subcan2  6992  ltadd1  7179  leadd2  7181  ltsubadd  7182  lesubadd  7184  ltaddsub2  7187  leaddsub2  7189  ltaddpos  7202  lesub2  7207  ltsub2  7209  ltnegcon1  7213  ltnegcon2  7214  lenegcon1  7216  lenegcon2  7217  addge01  7222  addge02  7223  suble0  7226  leaddle0  7227  lesub0  7229  recexre  7322  reaplt  7332  reapltxor  7333  reapneg  7341  remulext1  7343  apreim  7347  apcotr  7351  apadd2  7353  addext  7354  mulcanap2d  7385  diveqap0  7403  diveqap1  7424  ltmul2  7563  lemul2  7564  ltmulgt11  7571  ltmulgt12  7572  gt0div  7577  ge0div  7578  ltmuldiv  7581  ltrec1  7595  lerec2  7596  ledivdiv  7597  ltdiv23  7599  lediv23  7600  creur  7652  creui  7653  nn1suc  7674  nnrecl  7915  znnsub  8032  zgt0ge1  8038  zltlen  8055  nn0n0n1ge2b  8056  btwnnz  8070  gtndiv  8071  prime  8073  eluz2  8215  indstr2  8282  negm  8286  nn01to3  8288  qapne  8310  qreccl  8311  iccid  8524  elioc2  8535  elico2  8536  elicc2  8537  elfz2  8611  fzen  8637  fzsubel  8653  elfzp1  8664  fzpr  8669  fzrevral2  8698  fzrevral3  8699  nn0disj  8725  2ffzeq  8728  fzosplitsni  8821  frecuzrdgfn  8839  nn0ennn  8850  sq11  8939  cjap  9094  cbvrald  9196  bj-nalset  9280  bj-sels  9299  bj-nnelirr  9341
  Copyright terms: Public domain W3C validator