Theorem simp3r 1050

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

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

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 1004

This theorem is referenced by:  simpl3r  1077  simpr3r  1083  simp13r  1137  simp23r  1143  simp33r  1149  issod  4410  tfisi  4679  fvun1  5702  f1oiso2  5957  tfrlem5  6466  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  ecopovtrn  6787  ecopovtrng  6790  dftap2  7445  addassnqg  7577  ltsonq  7593  ltanqg  7595  ltmnqg  7596  addassnq0  7657  mulasssrg  7953  distrsrg  7954  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1lem  7975  mulextsr1  7976  axmulass  8068  axdistr  8069  reapmul1  8750  mulcanap  8820  mulcanap2  8821  divassap  8845  divdirap  8852  div11ap  8855  apmul1  8943  ltdiv1  9023  ltmuldiv  9029  ledivmul  9032  lemuldiv  9036  lediv2  9046  ltdiv23  9047  lediv23  9048  xaddass2  10074  xlt2add  10084  modqdi  10622  expaddzap  10813  expmulzap  10815  leisorel  11067  resqrtcl  11548  xrbdtri  11795  dvdsgcd  12541  rpexp12i  12685  pythagtriplem4  12799  pythagtriplem11  12805  pythagtriplem13  12807  pcpremul  12824  pceu  12826  pcqmul  12834  pcqdiv  12838  f1ocpbllem  13351  ercpbl  13372  erlecpbl  13373  cmn4  13850  ablsub4  13858  abladdsub4  13859  lidlsubcl  14459  psmetlecl  15016  xmetlecl  15049  xblcntrps  15095  xblcntr  15096