Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  biimpar GIF version

Theorem biimpar 281
 Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimpar ((𝜑𝜒) → 𝜓)

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimprd 147 . 2 (𝜑 → (𝜒𝜓))
32imp 115 1 ((𝜑𝜒) → 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ 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:  exbiri  364  bitr  441  eqtr  2057  opabss  3821  euotd  3991  wetriext  4301  sosng  4413  xpsspw  4450  brcogw  4504  funimaexglem  4982  funfni  4999  fnco  5007  fnssres  5012  fn0  5018  fnimadisj  5019  fnimaeq0  5020  foco  5116  foimacnv  5144  fvelimab  5229  fvopab3ig  5246  dff3im  5312  dffo4  5315  fmptco  5330  f1eqcocnv  5431  f1ocnv2d  5704  fnexALT  5740  xp1st  5792  xp2nd  5793  tfrlemiubacc  5944  tfri2d  5950  tfri3  5953  ecelqsg  6159  elqsn0m  6174  fidifsnen  6331  recclnq  6490  nq0a0  6555  qreccl  8576  difelfzle  8992  frec2uzlt2d  9190  caucvgrelemcau  9579  recvalap  9693  fzomaxdiflem  9708
 Copyright terms: Public domain W3C validator