Theorem an12s 843

Description: Swap two conjuncts in antecedent. The label suffix "s" means that an12 838 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.)

Hypothesis

Ref	Expression
an12s.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

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

Proof of Theorem an12s

Step	Hyp	Ref	Expression
1		an12 838	. 2 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
2		an12s.1	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	1, 2	sylbi 207	1 ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  anabsan2  863  1stconst  7265  2ndconst  7266  oecl  7617  oaass  7641  odi  7659  oen0  7666  oeworde  7673  ltexprlem4  9861  iccshftr  12306  iccshftl  12308  iccdil  12310  icccntr  12312  ndvdsadd  15134  eulerthlem2  15487  neips  20917  tx1stc  21453  filuni  21689  ufldom  21766  isch3  28098  unoplin  28779  hmoplin  28801  adjlnop  28945  chirredlem2  29250  btwnconn1lem12  32205  btwnconn1  32208  finxpreclem2  33227  poimirlem25  33434  mblfinlem4  33449  iscringd  33797  unichnidl  33830