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

Theorem biimp3a 1345
Description: Infer implication from a logical equivalence. Similar to biimpa 296. (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 296 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
323impa 1194 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  nnawordex  6527  div2subap  8790  nn0addge1  9218  nn0addge2  9219  nn0sub2  9322  eluzp1p1  9549  uznn0sub  9555  iocssre  9949  icossre  9950  iccssre  9951  lincmb01cmp  9999  iccf1o  10000  fzosplitprm1  10229  subfzo0  10237  modfzo0difsn  10390  efltim  11699  fldivndvdslt  11932  prmdiv  12227  hashgcdlem  12230  vfermltl  12243  coprimeprodsq  12249  pythagtrip  12275  difsqpwdvds  12329  tgtop11  13447  sinq12gt0  14122
  Copyright terms: Public domain W3C validator