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

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

Proof of Theorem 3expb
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1103 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp32 244 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:  3adant3r1  1113  3adant3r2  1114  3adant3r3  1115  3adant1l  1127  3adant1r  1128  mp3an1  1219  soinxp  4410  sotri  4720  fnfco  5065  mpt2eq3dva  5569  fovrnda  5644  ovelrn  5649  grprinvd  5696  nnmsucr  6067  ltpopr  6691  ltexprlemdisj  6702  recexprlemdisj  6726  mul4  7143  add4  7170  2addsub  7223  addsubeq4  7224  subadd4  7253  muladd  7379  ltleadd  7439  divmulap  7652  divap0  7661  div23ap  7668  div12ap  7671  divsubdirap  7682  divcanap5  7688  divmuleqap  7691  divcanap6  7693  divdiv32ap  7694  letrp1  7812  lemul12b  7825  lediv1  7833  cju  7911  nndivre  7947  nndivtr  7953  nn0addge1  8226  nn0addge2  8227  peano2uz2  8343  uzind  8347  uzind3  8349  fzind  8351  fnn0ind  8352  uzind4  8529  qre  8558  irrmul  8579  rpdivcl  8606  rerpdivcl  8611  iccshftr  8860  iccshftl  8862  iccdil  8864  icccntr  8866  fzaddel  8920  fzrev  8944  frec2uzf1od  9166  expdivap  9279  2shfti  9406  iisermulc2  9834
  Copyright terms: Public domain W3C validator