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  4113  tfisi  4368  fvun1  5318  f1oiso2  5548  tfrlem5  6014  tfr1onlembxssdm  6043  tfrcllembxssdm  6056  ecopovtrn  6322  ecopovtrng  6325  addassnqg  6862  ltsonq  6878  ltanqg  6880  ltmnqg  6881  addassnq0  6942  mulasssrg  7225  distrsrg  7226  lttrsr  7229  ltsosr  7231  ltasrg  7237  mulextsr1lem  7246  mulextsr1  7247  axmulass  7329  axdistr  7330  reapmul1  7990  mulcanap  8050  mulcanap2  8051  divassap  8073  divdirap  8080  div11ap  8083  apmul1  8171  ltdiv1  8241  ltmuldiv  8247  ledivmul  8250  lemuldiv  8254  lediv2  8264  ltdiv23  8265  lediv23  8266  modqdi  9702  expaddzap  9850  expmulzap  9852  resqrtcl  10303  dvdsgcd  10795  rpexp12i  10928
  Copyright terms: Public domain W3C validator