Theorem an4s 588

Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)

Hypothesis

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

Assertion

Ref	Expression
an4s	⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Proof of Theorem an4s

Step	Hyp	Ref	Expression
1		an4 586	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)))
2		an4s.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
3	1, 2	sylbi 121	1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  an42s  589  anandis  592  anandirs  593  trin2  5038  fnun  5341  2elresin  5346  f1co  5452  f1oun  5500  f1oco  5503  f1mpt  5793  poxp  6257  tfrlem7  6342  brecop  6651  th3qlem1  6663  oviec  6667  pmss12g  6701  addcmpblnq  7396  mulcmpblnq  7397  mulpipqqs  7402  mulclnq  7405  mulcanenq  7414  distrnqg  7416  mulcmpblnq0  7473  mulcanenq0ec  7474  mulclnq0  7481  nqnq0a  7483  nqnq0m  7484  distrnq0  7488  genipv  7538  genpelvl  7541  genpelvu  7542  genpml  7546  genpmu  7547  genpcdl  7548  genpcuu  7549  genprndl  7550  genprndu  7551  distrlem1prl  7611  distrlem1pru  7612  ltsopr  7625  addcmpblnr  7768  ltsrprg  7776  addclsr  7782  mulclsr  7783  addasssrg  7785  addresr  7866  mulresr  7867  axaddass  7901  axmulass  7902  axdistr  7903  mulgt0  8062  mul4  8119  add4  8148  2addsub  8201  addsubeq4  8202  sub4  8232  muladd  8371  mulsub  8388  add20i  8479  mulge0i  8607  mulap0b  8642  divmuldivap  8699  ltmul12a  8847  zmulcl  9336  uz2mulcl  9638  qaddcl  9665  qmulcl  9667  qreccl  9672  rpaddcl  9707  ge0addcl  10011  ge0xaddcl  10013  expge1  10588  rexanuz  11029  amgm2  11159  iooinsup  11317  mulcn2  11352  dvds2ln  11863  opoe  11932  omoe  11933  opeo  11934  omeo  11935  lcmgcd  12110  lcmdvds  12111  pc2dvds  12362  tgcl  14024  innei  14123  txbas  14218  txss12  14226  txbasval  14227  blsscls2  14453  qtopbasss  14481  lgslem3  14864  bj-indind  15145