Theorem simp1l 1052

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp1l	|- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

Proof of Theorem simp1l

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ph /\ ps ) -> ph )
2	1	3ad2ant1 1049	1 |- ( ( ( ph /\ ps ) /\ ch /\ th ) -> ph )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1l  1079  simpr1l  1085  simp11l  1139  simp21l  1145  simp31l  1151  en2lp  4701  tfisi  4734  funprg  5431  nnsucsssuc  6765  ecopovtrn  6906  ecopovtrng  6909  addassnqg  7749  distrnqg  7754  ltsonq  7765  ltanqg  7767  ltmnqg  7768  distrnq0  7826  addassnq0  7829  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  dmdcanap  9052  lt2msq1  9215  ltdiv2  9217  lediv2  9221  xaddass  10271  xaddass2  10272  xlt2add  10282  modqdi  10829  expaddzaplem  11019  expaddzap  11020  expmulzap  11022  swrdspsleq  11439  pfxeq  11468  ccatopth2  11489  pfxccat3  11506  resqrtcl  11795  bdtrilem  12005  bdtri  12006  xrbdtri  12042  bitsfzo  12722  prmexpb  12929  4sqlem18  13187  subgabl  14136  rng1zrlem  14258  opprringbg  14385  cnptoprest  15340  ssblps  15526  ssbl  15527  plyadd  15852  plymul  15853  rplogbchbase  16052  rplogbreexp  16055  relogbcxpbap  16067  lgssq  16159  uhgr2edg  16447  clwwlkccat  16642