Theorem impancom 455

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 449	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 84	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	imp 444	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  eqrdav  2609  rexraleqim  3299  disjiun  4573  propeqop  4895  euotd  4900  pwssun  4944  funopsn  6319  isotr  6486  el2mpt2csbcl  7137  ressuppssdif  7203  oeordi  7554  domunsncan  7945  pssnn  8063  findcard3  8088  ordtypelem7  8312  inf3lem5  8412  r1tr  8522  cardmin2  8707  ac10ct  8740  isf32lem12  9069  isfin1-3  9091  fin17  9099  fin1a2s  9119  axdc4lem  9160  axcclem  9162  ttukeylem2  9215  genpcd  9707  ltexprlem3  9739  prlem936  9748  supsrlem  9811  mul0or  10546  fiminre  10851  un0addcl  11203  un0mulcl  11204  btwnnz  11329  uznfz  12292  elfz0ubfz0  12312  elfzo0z  12377  fzofzim  12382  elfzom1p1elfzo  12414  ssfzoulel  12428  ssfzo12bi  12429  subfzo0  12452  modmuladdim  12575  modaddmodup  12595  modfzo0difsn  12604  axdc4uzlem  12644  expaddz  12766  sq01  12848  hashnn0n0nn  13041  hashss  13058  hashgt12el  13070  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  ccatalpha  13228  swrdswrdlem  13311  swrdswrd  13312  swrdccatin1  13334  swrdccatin12lem3  13341  repswswrd  13382  cshwmodn  13392  cshf1  13407  cshw1  13419  2cshwcshw  13422  sqrmo  13840  caubnd2  13945  summo  14295  nno  14936  divalglem8  14961  lcmdvds  15159  lcmfunsnlem1  15188  hashgcdeq  15332  modprm0  15348  pcqcl  15399  vdwnnlem3  15539  prmgaplem5  15597  prmgaplem7  15599  catpropd  16192  cicsym  16287  isinitoi  16476  istermoi  16477  iszeroi  16482  acsfiindd  17000  tsrlemax  17043  issubg4  17436  gsmsymgreqlem2  17674  oddvdsnn0  17786  oddvds  17789  gexdvds  17822  lt6abl  18119  pgpfac1lem3  18299  coe1ae0  19407  isphld  19818  mdetdiaglem  20223  slesolex  20307  pmatcoe1fsupp  20325  cpmatelimp  20336  cpmatelimp2  20338  cpmatmcllem  20342  pm2mpf1  20423  mp2pm2mplem4  20433  fvmptnn04ifa  20474  fvmptnn04ifd  20477  chfacfscmul0  20482  chfacfpmmul0  20486  neii1  20720  neii2  20722  uncmp  21016  isfild  21472  fbunfip  21483  fgss2  21488  fgcl  21492  isufil2  21522  cfinufil  21542  ufilen  21544  fsumcn  22481  lmmbr  22864  iscau4  22885  caussi  22903  ovoliunnul  23082  ovolicc2lem4  23095  itg1ge0a  23284  rolle  23557  ulmcaulem  23952  cxpge0  24229  fsumvma  24738  gausslemma2dlem1a  24890  2sqb  24957  pntrsumbnd2  25056  pntlem3  25098  axeuclid  25643  axcontlem2  25645  upgredg  25811  nbcusgra  25992  cusgrares  26001  usgrasscusgra  26011  sizeusglecusglem1  26012  usgrwlknloop  26093  wlkdvspthlem  26137  usgra2wlkspthlem2  26148  fargshiftf  26164  wwlknimp  26215  wlkiswwlk2lem5  26223  vfwlkniswwlkn  26234  usg2wlkeq  26236  wlkiswwlksur  26247  clwwlkgt0  26299  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwwlkel  26321  wwlksubclwwlk  26332  clwwisshclwwlem1  26333  clwlkfoclwwlk  26372  usg2spthonot0  26416  vdgn1frgrav3  26555  frgrancvvdeqlem3  26559  frgrancvvdeqlem4  26560  extwwlkfablem2  26605  numclwwlkun  26606  numclwwlkovf2ex  26613  frgraregord013  26645  spansncvi  27895  lnconi  28276  cdj3lem1  28677  spc2ed  28696  metider  29265  nofv  31054  sltres  31061  finminlem  31482  clsint2  31494  bj-finsumval0  32324  finxpsuclem  32410  wl-exeq  32500  phpreu  32563  poimirlem26  32605  poimir  32612  ismtyima  32772  elpaddn0  34104  tendospcanN  35330  rexzrexnn0  36386  unxpwdom3  36683  fsovrfovd  37323  radcnvrat  37535  2pwp1prm  40041  lighneal  40066  zm1nn  40348  subsubelfzo0  40359  fzoopth  40360  2ffzoeq  40361  usgrislfuspgr  40414  nbuhgr2vtx1edgblem  40573  usgredgsscusgredg  40675  upgr1wlkvtxedg  40853  uspgr2wlkeq  40854  uspgrn2crct  41011  crctcsh1wlkn0lem4  41016  1wlkiswwlks2lem5  41070  wlknewwlksn  41084  wlkwwlksur  41094  umgrwwlks2on  41161  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwwlksel  41221  wwlksubclwwlks  41232  clwwisshclwwslemlem  41233  clwlksfoclwwlk  41270  uhgr3cyclexlem  41348  vdgn1frgrv3  41467  frgrncvvdeqlem3  41471  frgrncvvdeqlem4  41472  av-numclwwlkovf2ex  41517  av-frgraregord013  41549  isassintop  41636  uzlidlring  41719  2zrngamgm  41729  ply1mulgsumlem1  41968  suppdm  42094