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

Theorem 3expia 1168
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 1165 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 123 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:  mp3an3  1289  3gencl  2694  moi  2840  sotricim  4215  elirr  4426  en2lp  4439  suc11g  4442  3optocl  4587  sefvex  5410  f1oresrab  5553  ovmpos  5862  ov2gf  5863  poxp  6097  brtposg  6119  dfsmo2  6152  smoiun  6166  tfrlemibxssdm  6192  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  nnsucsssuc  6356  nnaordi  6372  nnawordex  6392  mapvalg  6520  pmvalg  6521  elmapg  6523  xpdom3m  6696  ordiso  6889  ctssdc  6966  pr2ne  7016  ltbtwnnqq  7191  prarloclem4  7274  addlocpr  7312  1idprl  7366  1idpru  7367  ltexprlemrnd  7381  recexprlemrnd  7405  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1l  7411  recexprlemss1u  7412  aptisr  7555  axpre-apti  7661  ltxrlt  7798  axapti  7803  lttri3  7812  reapti  8309  apreap  8317  msqge0  8346  mulge0  8349  recexap  8382  mulap0b  8384  lt2msq  8612  zaddcl  9062  zdiv  9107  zextlt  9111  prime  9118  uzind2  9131  fzind  9134  lbzbi  9376  xltneg  9587  xlt2add  9631  iocssre  9704  icossre  9705  iccssre  9706  fzen  9791  rebtwn2zlemshrink  9999  qbtwnxr  10003  ioo0  10005  ioom  10006  ico0  10007  ioc0  10008  expclzaplem  10285  expnegzap  10295  expaddzap  10305  expmulzap  10307  omgadd  10516  shftuz  10557  cau3lem  10854  climuni  11030  efltim  11331  divalgb  11549  ndvdssub  11554  dvdsgcd  11627  lcmgcdlem  11685  qredeu  11705  isprm3  11726  prmdvdsexpr  11755  prmexpb  11756  ctinf  11870  cnntr  12321  cncnp2m  12327  cnptoprest  12335  lmtopcnp  12346  cnmptcom  12394  hmeof1o  12405  blpnf  12496  blssps  12523  blss  12524  blssec  12534  neibl  12587  climcncf  12667  cnplimcim  12732  bj-peano4  13080  triap  13151
  Copyright terms: Public domain W3C validator