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

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

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 108 . 2 ((𝜒𝜃) → 𝜃)
213ad2ant3 964 1 ((𝜑𝜓 ∧ (𝜒𝜃)) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
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 924
This theorem is referenced by:  simpl3r  997  simpr3r  1003  simp13r  1057  simp23r  1063  simp33r  1069  issod  4119  tfisi  4374  fvun1  5327  f1oiso2  5561  tfrlem5  6027  tfr1onlembxssdm  6056  tfrcllembxssdm  6069  ecopovtrn  6335  ecopovtrng  6338  addassnqg  6878  ltsonq  6894  ltanqg  6896  ltmnqg  6897  addassnq0  6958  mulasssrg  7241  distrsrg  7242  lttrsr  7245  ltsosr  7247  ltasrg  7253  mulextsr1lem  7262  mulextsr1  7263  axmulass  7345  axdistr  7346  reapmul1  8006  mulcanap  8066  mulcanap2  8067  divassap  8089  divdirap  8096  div11ap  8099  apmul1  8187  ltdiv1  8257  ltmuldiv  8263  ledivmul  8266  lemuldiv  8270  lediv2  8280  ltdiv23  8281  lediv23  8282  modqdi  9720  expaddzap  9890  expmulzap  9892  leisorel  10131  resqrtcl  10350  dvdsgcd  10868  rpexp12i  11001
  Copyright terms: Public domain W3C validator