Theorem simp3r 1053

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

Assertion

Ref	Expression
simp3r	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Proof of Theorem simp3r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 1047	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  simpl3r  1080  simpr3r  1086  simp13r  1140  simp23r  1146  simp33r  1152  issod  4439  tfisi  4708  fvun1  5742  f1oiso2  5999  tfrlem5  6544  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  ecopovtrn  6865  ecopovtrng  6868  dftap2  7564  addassnqg  7696  ltsonq  7712  ltanqg  7714  ltmnqg  7715  addassnq0  7776  mulasssrg  8072  distrsrg  8073  lttrsr  8076  ltsosr  8078  ltasrg  8084  mulextsr1lem  8094  mulextsr1  8095  axmulass  8187  axdistr  8188  reapmul1  8868  mulcanap  8938  mulcanap2  8939  divassap  8963  divdirap  8970  div11ap  8973  apmul1  9061  ltdiv1  9141  ltmuldiv  9147  ledivmul  9150  lemuldiv  9154  lediv2  9164  ltdiv23  9165  lediv23  9166  xaddass2  10202  xlt2add  10212  modqdi  10753  expaddzap  10944  expmulzap  10946  leisorel  11205  resqrtcl  11710  xrbdtri  11957  dvdsgcd  12704  rpexp12i  12848  pythagtriplem4  12962  pythagtriplem11  12968  pythagtriplem13  12970  pcpremul  12987  pceu  12989  pcqmul  12997  pcqdiv  13001  f1ocpbllem  13515  ercpbl  13536  erlecpbl  13537  cmn4  14014  ablsub4  14022  abladdsub4  14023  lidlsubcl  14627  psmetlecl  15191  xmetlecl  15224  xblcntrps  15270  xblcntr  15271