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

Theorem simp3r 1011
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp3r ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 109 . 2 ((𝜒𝜃) → 𝜃)
213ad2ant3 1005 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  simpl3r  1038  simpr3r  1044  simp13r  1098  simp23r  1104  simp33r  1110  issod  4248  tfisi  4508  fvun1  5494  f1oiso2  5735  tfrlem5  6218  tfr1onlembxssdm  6247  tfrcllembxssdm  6260  ecopovtrn  6533  ecopovtrng  6536  addassnqg  7213  ltsonq  7229  ltanqg  7231  ltmnqg  7232  addassnq0  7293  mulasssrg  7589  distrsrg  7590  lttrsr  7593  ltsosr  7595  ltasrg  7601  mulextsr1lem  7611  mulextsr1  7612  axmulass  7704  axdistr  7705  reapmul1  8380  mulcanap  8449  mulcanap2  8450  divassap  8473  divdirap  8480  div11ap  8483  apmul1  8571  ltdiv1  8649  ltmuldiv  8655  ledivmul  8658  lemuldiv  8662  lediv2  8672  ltdiv23  8673  lediv23  8674  xaddass2  9682  xlt2add  9692  modqdi  10195  expaddzap  10367  expmulzap  10369  leisorel  10611  resqrtcl  10832  xrbdtri  11076  dvdsgcd  11734  rpexp12i  11867  psmetlecl  12540  xmetlecl  12573  xblcntrps  12619  xblcntr  12620
  Copyright terms: Public domain W3C validator