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

Theorem 3expia 1141
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expia ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem 3expia
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1138 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 122 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  mp3an3  1258  3gencl  2634  moi  2776  sotricim  4086  elirr  4292  en2lp  4305  suc11g  4308  3optocl  4444  sefvex  5227  f1oresrab  5361  ovmpt2s  5655  ov2gf  5656  poxp  5884  brtposg  5903  dfsmo2  5936  smoiun  5950  tfrlemibxssdm  5976  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemaccex  5997  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemaccex  6010  tfrcllemres  6011  tfrcl  6013  nnsucsssuc  6136  nnaordi  6147  nnawordex  6167  xpdom3m  6378  ordiso  6506  pr2ne  6520  ltbtwnnqq  6667  prarloclem4  6750  addlocpr  6788  1idprl  6842  1idpru  6843  ltexprlemrnd  6857  recexprlemrnd  6881  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1l  6887  recexprlemss1u  6888  aptisr  7017  axpre-apti  7113  ltxrlt  7245  axapti  7250  lttri3  7258  reapti  7746  apreap  7754  msqge0  7783  mulge0  7786  recexap  7810  mulap0b  7812  lt2msq  8031  zaddcl  8472  zdiv  8516  zextlt  8520  prime  8527  uzind2  8540  fzind  8543  lbzbi  8782  xltneg  8979  iocssre  9052  icossre  9053  iccssre  9054  fzen  9138  rebtwn2zlemshrink  9340  qbtwnxr  9344  ioo0  9346  ioom  9347  ico0  9348  ioc0  9349  expival  9575  expclzaplem  9597  expnegzap  9607  expaddzap  9617  expmulzap  9619  omgadd  9826  shftuz  9843  cau3lem  10138  climuni  10270  divalgb  10469  ndvdssub  10474  dvdsgcd  10545  lcmgcdlem  10603  qredeu  10623  isprm3  10644  prmdvdsexpr  10673  prmexpb  10674  bj-peano4  10935
  Copyright terms: Public domain W3C validator