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

Theorem biimp3ar 1467
 Description: Infer implication from a logical equivalence. Similar to biimpar 481. (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 1108 1 ((𝜑𝜓𝜃) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  rmoi  3822  brelrng  5781  div2sub  11472  nn0p1elfzo  13095  ssfzo12  13145  modltm1p1mod  13306  hashgt23el  13801  repswpfx  14158  abssubge0  14699  qredeu  16012  abvne0  19612  slesolinvbi  21327  basgen2  21635  fcfval  22679  nmne0  23266  ovolfsf  24116  logbprmirr  25426  lgssq  25965  lgssq2  25966  colinearalg  26748  usgr0v  27075  frgr0vb  28092  nv1  28502  adjeq  29762  pridln1  31087  revpfxsfxrev  32541  fpr3g  33305  frrlem4  33309  areacirc  35301  fvopabf4g  35310  exidreslem  35466  hgmapvvlem3  39372  iocmbl  40334  iunconnlem2  41812  ssfz12  44039  m1modmmod  45101
 Copyright terms: Public domain W3C validator