Theorem simp3r 978

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 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	3ad2ant3 972	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 930

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

This theorem depends on definitions:  df-bi 116  df-3an 932

This theorem is referenced by:  simpl3r  1005  simpr3r  1011  simp13r  1065  simp23r  1071  simp33r  1077  issod  4179  tfisi  4439  fvun1  5419  f1oiso2  5660  tfrlem5  6141  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  ecopovtrn  6456  ecopovtrng  6459  addassnqg  7091  ltsonq  7107  ltanqg  7109  ltmnqg  7110  addassnq0  7171  mulasssrg  7454  distrsrg  7455  lttrsr  7458  ltsosr  7460  ltasrg  7466  mulextsr1lem  7475  mulextsr1  7476  axmulass  7558  axdistr  7559  reapmul1  8223  mulcanap  8287  mulcanap2  8288  divassap  8311  divdirap  8318  div11ap  8321  apmul1  8409  ltdiv1  8484  ltmuldiv  8490  ledivmul  8493  lemuldiv  8497  lediv2  8507  ltdiv23  8508  lediv23  8509  xaddass2  9494  xlt2add  9504  modqdi  10006  expaddzap  10178  expmulzap  10180  leisorel  10421  resqrtcl  10641  xrbdtri  10884  dvdsgcd  11493  rpexp12i  11626  psmetlecl  12262  xmetlecl  12295  xblcntrps  12341  xblcntr  12342