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

Theorem 3impia 1141
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impia.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
3impia ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impia
StepHypRef Expression
1 3impia.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 114 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1138 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  mopick2  2032  3gencl  2654  mob2  2796  moi  2799  reupick3  3285  disjne  3340  disji2  3844  tz7.2  4190  funopg  5061  fvun1  5383  fvopab6  5410  isores3  5608  ovmpt4g  5781  ovmpt2s  5782  ov2gf  5783  ofrval  5880  poxp  6011  smoel  6079  tfr1onlemaccex  6127  tfrcllemaccex  6140  nnaass  6260  qsel  6383  xpdom3m  6604  phpm  6635  prarloclem3  7117  aptisr  7385  axpre-apti  7481  axapti  7618  addn0nid  7913  divvalap  8202  letrp1  8370  p1le  8371  zextle  8898  zextlt  8899  btwnnz  8901  gtndiv  8902  uzind2  8919  fzind  8922  iccleub  9410  uzsubsubfz  9522  elfz0fzfz0  9598  difelfznle  9607  elfzo0le  9657  fzonmapblen  9659  fzofzim  9660  fzosplitprm1  9706  rebtwn2zlemstep  9725  qbtwnxr  9730  expcl2lemap  10028  expclzaplem  10040  expnegzap  10050  leexp2r  10070  expnbnd  10138  bcval4  10221  bccmpl  10223  absexpzap  10574  divalgb  11264  ndvdssub  11269  dvdsgcd  11340  dfgcd2  11342  rplpwr  11355  lcmgcdlem  11398  coprmdvds1  11412  qredeq  11417  prmdvdsexpr  11468  elrestr  11721
  Copyright terms: Public domain W3C validator