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

Theorem 3impia 1163
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 1160 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947
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 949
This theorem is referenced by:  mopick2  2060  3gencl  2694  mob2  2837  moi  2840  reupick3  3331  disjne  3386  disji2  3892  tz7.2  4246  funopg  5127  fvun1  5455  fvopab6  5485  isores3  5684  ovmpt4g  5861  ovmpos  5862  ov2gf  5863  ofrval  5960  poxp  6097  smoel  6165  tfr1onlemaccex  6213  tfrcllemaccex  6226  nnaass  6349  qsel  6474  xpdom3m  6696  phpm  6727  ctssdc  6966  mkvprop  7000  prarloclem3  7273  aptisr  7555  axpre-apti  7661  axapti  7803  addn0nid  8104  divvalap  8402  letrp1  8574  p1le  8575  zextle  9110  zextlt  9111  btwnnz  9113  gtndiv  9114  uzind2  9131  fzind  9134  iccleub  9682  uzsubsubfz  9795  elfz0fzfz0  9871  difelfznle  9880  elfzo0le  9930  fzonmapblen  9932  fzofzim  9933  fzosplitprm1  9979  rebtwn2zlemstep  9998  qbtwnxr  10003  expcl2lemap  10273  expclzaplem  10285  expnegzap  10295  leexp2r  10315  expnbnd  10383  bcval4  10466  bccmpl  10468  absexpzap  10820  divalgb  11549  ndvdssub  11554  dvdsgcd  11627  dfgcd2  11629  rplpwr  11642  lcmgcdlem  11685  coprmdvds1  11699  qredeq  11704  prmdvdsexpr  11755  elrestr  12055  mopni  12578  sincosq1lem  12833
  Copyright terms: Public domain W3C validator