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  4445  tfisi  4714  fvun1  5748  f1oiso2  6006  tfrlem5  6558  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  ecopovtrn  6879  ecopovtrng  6882  dftap2  7581  addassnqg  7713  ltsonq  7729  ltanqg  7731  ltmnqg  7732  addassnq0  7793  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  reapmul1  8887  mulcanap  8957  mulcanap2  8958  divassap  8984  divdirap  8991  div11ap  8994  apmul1  9082  ltdiv1  9162  ltmuldiv  9168  ledivmul  9171  lemuldiv  9175  lediv2  9185  ltdiv23  9186  lediv23  9187  xaddass2  10225  xlt2add  10235  modqdi  10781  expaddzap  10972  expmulzap  10974  leisorel  11237  resqrtcl  11743  xrbdtri  11990  dvdsgcd  12737  rpexp12i  12881  pythagtriplem4  12995  pythagtriplem11  13001  pythagtriplem13  13003  pcpremul  13020  pceu  13022  pcqmul  13030  pcqdiv  13034  f1ocpbllem  13578  ercpbl  13599  erlecpbl  13600  cmn4  14062  ablsub4  14070  abladdsub4  14071  lidlsubcl  14765  psmetlecl  15329  xmetlecl  15362  xblcntrps  15408  xblcntr  15409