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

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 is referenced by:  eqrdav  2228  disjiun  4078  euotd  4341  onsucelsucr  4600  isotr  5946  spc2ed  6385  nninfninc  7301  ltbtwnnqq  7613  genpcdl  7717  genpcuu  7718  un0addcl  9413  un0mulcl  9414  btwnnz  9552  uznfz  10311  elfz0ubfz0  10333  fzoss1  10381  elfzo0z  10396  fzofzim  10400  elfzom1p1elfzo  10432  ssfzo12bi  10443  subfzo0  10460  modfzo0difsn  10629  expaddzap  10817  ccatalpha  11161  swrdswrdlem  11251  swrdswrd  11252  swrdccatin1  11272  pfxccatin12lem3  11279  caucvgre  11507  caubnd2  11643  summodc  11909  fzo0dvdseq  12383  nno  12432  lcmdvds  12616  hashgcdeq  12777  modprm0  12792  pcqcl  12844  issubg4m  13745  01eq0ring  14168  neii1  14836  neii2  14838  fsumcncntop  15256  gausslemma2dlem1a  15752  usgrislfuspgrdom  16003  upgrwlkvtxedg  16105  uspgr2wlkeq  16106  clwwlkccatlem  16137