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

Theorem biimp3ar 1471
Description: Infer implication from a logical equivalence. Similar to biimpar 477. (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 810 . 2 (𝜑 → (𝜓 → (𝜃𝜒)))
323imp 1110 1 ((𝜑𝜓𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  rmoi  3890  brelrng  5951  fpr3g  8311  frrlem4  8315  dif1enlem  9197  dif1enlemOLD  9198  php3  9250  div2sub  12093  nn0p1elfzo  13743  ssfzo12  13799  modltm1p1mod  13965  hashgt23el  14464  repswpfx  14824  abssubge0  15367  qredeu  16696  abvne0  20821  slesolinvbi  22688  basgen2  22997  fcfval  24042  nmne0  24633  ovolfsf  25507  logbprmirr  26840  lgssq  27382  lgssq2  27383  colinearalg  28926  usgr0v  29259  frgr0vb  30283  nv1  30695  adjeq  31955  pridln1  33472  revpfxsfxrev  35122  areacirc  37721  fvopabf4g  37730  exidreslem  37885  hgmapvvlem3  41928  iocmbl  43230  iunconnlem2  44960  ssfz12  47331  m1modmmod  48447
  Copyright terms: Public domain W3C validator