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

Theorem 3expa 1104
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expa (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1103 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp31 243 1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  3anidm23  1194  mp3an2  1220  mpd3an3  1233  rgen3  2406  moi2  2722  sbc3ie  2831  preq12bg  3544  issod  4056  wepo  4096  reuhypd  4203  funimass4  5224  fvtp1g  5369  f1imass  5413  fcof1o  5429  f1ofveu  5500  f1ocnvfv3  5501  acexmid  5511  2ndrn  5809  rdgon  5973  frecrdg  5992  findcard  6345  findcard2  6346  findcard2s  6347  ltapig  6434  ltanqi  6498  ltmnqi  6499  lt2addnq  6500  lt2mulnq  6501  prarloclemcalc  6598  genpassl  6620  genpassu  6621  prmuloc  6662  ltexprlemm  6696  ltexprlemfl  6705  ltexprlemfu  6707  lteupri  6713  ltaprg  6715  mul4  7143  add4  7170  cnegexlem2  7185  cnegexlem3  7186  2addsub  7223  addsubeq4  7224  muladd  7379  ltleadd  7439  reapmul1  7584  apreim  7592  receuap  7648  p1le  7813  lemul12b  7825  zdiv  8326  fzind  8351  fnn0ind  8352  uzss  8491  qmulcl  8570  qreccl  8574  xrlttr  8714  icc0r  8793  iooshf  8819  elfz5  8880  elfz0fzfz0  8981  fzind2  9093  expnegap0  9237  expineg2  9238  mulexpzap  9269  expsubap  9276  expnbnd  9346  crim  9432  climshftlemg  9797
  Copyright terms: Public domain W3C validator