MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp22l Structured version   Visualization version   GIF version

Theorem simp22l 1375
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp22l ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

Proof of Theorem simp22l
StepHypRef Expression
1 simp2l 1240 . 2 ((𝜒 ∧ (𝜑𝜓) ∧ 𝜃) → 𝜑)
213ad2ant2 1127 1 ((𝜏 ∧ (𝜒 ∧ (𝜑𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1072
This theorem is referenced by:  ax5seglem6  26034  segconeu  32449  3atlem2  35285  lplncvrlvol2  35416  paddasslem15  35635  4atex  35877  trlval4  35990  cdlemc5  35997  cdlemc6  35998  cdlemd2  36001  cdlemd3  36002  cdlemd4  36003  cdleme0moN  36027  cdleme3g  36036  cdleme3h  36037  cdleme3  36039  cdleme11g  36067  cdleme11h  36068  cdleme11j  36069  cdleme11k  36070  cdleme11l  36071  cdleme11  36072  cdleme14  36075  cdleme15a  36076  cdleme15c  36078  cdleme15d  36079  cdleme15  36080  cdleme16b  36081  cdleme16c  36082  cdleme16d  36083  cdleme16e  36084  cdleme16f  36085  cdleme18a  36093  cdleme18b  36094  cdleme18c  36095  cdleme19b  36106  cdleme19e  36109  cdleme20bN  36112  cdleme20c  36113  cdleme20d  36114  cdleme20e  36115  cdleme20f  36116  cdleme20g  36117  cdleme20h  36118  cdleme20j  36120  cdleme20l2  36123  cdleme20l  36124  cdleme20m  36125  cdleme21ct  36131  cdleme22d  36145  cdleme22e  36146  cdleme22eALTN  36147  cdleme26e  36161  cdleme27a  36169  cdleme28a  36172  cdleme30a  36180  cdleme43fsv1snlem  36222  cdlemefs44  36228  cdlemefs45ee  36232  cdleme35sn2aw  36260  cdleme36a  36262  cdleme39n  36268  cdleme40m  36269  cdleme42k  36286  cdlemeg47rv2  36312  cdlemeg46frv  36327  cdlemeg46vrg  36329  cdlemeg46rgv  36330  cdlemeg46req  36331  cdlemg2fv2  36402  cdlemg4g  36418  cdlemg4  36419  cdlemg6c  36422  cdlemg8b  36430  cdlemg8c  36431  cdlemg9a  36434  cdlemg9b  36435  cdlemg9  36436  cdlemg12a  36445  cdlemg12b  36446  cdlemg12c  36447  cdlemg17h  36470  cdlemg18b  36481  cdlemg18c  36482  cdlemg31b0a  36497  cdlemg27b  36498  cdlemg31d  36502  cdlemg28b  36505  cdlemg33a  36508  cdlemg33b  36509  cdlemg33c  36510  cdlemg33d  36511  cdlemg33e  36512  cdlemg33  36513  cdlemh  36619  cdlemk6  36639  cdlemki  36643  cdlemksat  36648  cdlemksv2  36649  cdlemk7  36650  cdlemk11  36651  cdlemk12  36652  cdlemkole  36655  cdlemk14  36656  cdlemk15  36657  cdlemk17  36660  cdlemk1u  36661  cdlemk5u  36663  cdlemk6u  36664  cdlemk7u  36672  cdlemk11u  36673  cdlemk12u  36674  cdlemk7u-2N  36690  cdlemk11u-2N  36691  cdlemk12u-2N  36692  cdlemk20-2N  36694  cdlemk28-3  36710  cdlemk33N  36711  cdlemk34  36712  cdlemk37  36716  cdlemk39  36718  cdlemk35s  36739  cdlemk39s  36741  cdlemk47  36751  cdlemk48  36752  cdlemk50  36754  cdlemk51  36755  cdlemk52  36756  cdlemkyyN  36764  cdlemk43N  36765  cdlemn2  36998  cdlemn10  37009
  Copyright terms: Public domain W3C validator