Theorem impancom 260

Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem impancom

Step	Hyp	Ref	Expression
1		impancom.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	ex 115	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 124	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  eqrdav  2237  disjiun  4125  euotd  4395  onsucelsucr  4655  isotr  6022  spc2ed  6469  nninfninc  7463  ltbtwnnqq  7782  genpcdl  7886  genpcuu  7887  un0addcl  9600  un0mulcl  9601  btwnnz  9744  uznfz  10520  elfz0ubfz0  10542  fzoss1  10590  elfzo0z  10606  fzofzim  10610  elfzom1p1elfzo  10642  ssfzo12bi  10653  subfzo0  10671  modfzo0difsn  10845  expaddzap  11033  ccatalpha  11395  swrdswrdlem  11490  swrdswrd  11491  swrdccatin1  11511  pfxccatin12lem3  11518  caucvgre  11761  caubnd2  11898  summodc  12166  fzo0dvdseq  12640  nno  12689  lcmdvds  12873  hashgcdeq  13038  modprm0  13053  pcqcl  13105  issubg4m  14045  01eq0ring  14545  neii1  15297  neii2  15299  fsumcncntop  15717  gausslemma2dlem1a  16275  usgrislfuspgrdom  16529  upgrwlkvtxedg  16703  uspgr2wlkeq  16704  clwwlkccatlem  16739  clwwlknonex2lem2  16777