Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimp3ar Structured version   Visualization version   GIF version

Theorem biimp3ar 1430
 Description: Infer implication from a logical equivalence. Similar to biimpar 502. (Contributed by NM, 2-Jan-2009.)
Hypothesis
Ref Expression
biimp3a.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
biimp3ar ((𝜑𝜓𝜃) → 𝜒)

Proof of Theorem biimp3ar
StepHypRef Expression
1 biimp3a.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21exbiri 651 . 2 (𝜑 → (𝜓 → (𝜃𝜒)))
323imp 1254 1 ((𝜑𝜓𝜃) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038 This theorem is referenced by:  rmoi  3516  brelrng  5325  div2sub  10810  nn0p1elfzo  12467  ssfzo12  12518  modltm1p1mod  12678  abssubge0  14017  qredeu  15315  abvne0  18767  slesolinvbi  20427  basgen2  20733  fcfval  21777  nmne0  22363  ovolfsf  23180  lgssq  24996  lgssq2  24997  colinearalg  25724  usgr0v  26060  frgr0vb  27026  nv1  27418  adjeq  28682  areacirc  33176  fvopabf4g  33186  exidreslem  33347  hgmapvvlem3  36736  iocmbl  37318  iunconnlem2  38693  ssfz12  40651  m1modmmod  41634
 Copyright terms: Public domain W3C validator