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

Theorem biimp3a 1306
Description: Infer implication from a logical equivalence. Similar to biimpa 292. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
biimp3a.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
biimp3a ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem biimp3a
StepHypRef Expression
1 biimp3a.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21biimpa 292 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1159 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  nnawordex  6390  div2subap  8556  nn0addge1  8974  nn0addge2  8975  nn0sub2  9075  eluzp1p1  9300  uznn0sub  9306  iocssre  9676  icossre  9677  iccssre  9678  lincmb01cmp  9726  iccf1o  9727  fzosplitprm1  9951  subfzo0  9959  modfzo0difsn  10108  efltim  11303  fldivndvdslt  11528  hashgcdlem  11798  tgtop11  12140
  Copyright terms: Public domain W3C validator