Theorem simp3r 1057

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 1051	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

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:  simpl3r  1084  simpr3r  1090  simp13r  1144  simp23r  1150  simp33r  1156  issod  4466  tfisi  4736  fvun1  5772  f1oiso2  6036  tfrlem5  6590  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  ecopovtrn  6911  ecopovtrng  6914  dftap2  7624  addassnqg  7756  ltsonq  7772  ltanqg  7774  ltmnqg  7775  addassnq0  7836  mulasssrg  8132  distrsrg  8133  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1lem  8154  mulextsr1  8155  axmulass  8247  axdistr  8248  reapmul1  8932  mulcanap  9002  mulcanap2  9003  divassap  9029  divdirap  9036  div11ap  9039  apmul1  9127  ltdiv1  9207  ltmuldiv  9213  ledivmul  9216  lemuldiv  9220  lediv2  9230  ltdiv23  9231  lediv23  9232  xaddass2  10289  xlt2add  10299  modqdi  10850  expaddzap  11041  expmulzap  11043  leisorel  11311  resqrtcl  11817  xrbdtri  12067  dvdsgcd  12814  rpexp12i  12959  pythagtriplem4  13076  pythagtriplem11  13082  pythagtriplem13  13084  pcpremul  13101  pceu  13103  pcqmul  13111  pcqdiv  13115  f1ocpbllem  13690  ercpbl  13711  erlecpbl  13712  cmn4  14198  ablsub4  14207  abladdsub4  14208  lidlsubcl  14933  psmetlecl  15593  xmetlecl  15626  xblcntrps  15672  xblcntr  15673