Theorem impancom 454

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mo4  2650  eqrdav  2822  spc2ed  3604  rexraleqim  3642  disjiun  5055  disjord  5056  disjiund  5058  propeqop  5399  euotd  5405  pwssun  5458  iotan0  6347  funopsn  6912  isotr  7091  funfv1st2nd  7747  funelss  7748  el2mpocsbcl  7782  ressuppssdif  7853  oeordi  8215  domunsncan  8619  pssnn  8738  findcard3  8763  ordtypelem7  8990  inf3lem5  9097  r1tr  9207  cardmin2  9429  ac10ct  9462  isf32lem12  9788  isfin1-3  9810  fin17  9818  fin1a2s  9838  axdc4lem  9879  axcclem  9881  ttukeylem2  9934  genpcd  10430  ltexprlem3  10462  prlem936  10471  supsrlem  10535  mul0or  11282  fiminreOLD  11592  un0addcl  11933  un0mulcl  11934  btwnnz  12061  uznfz  12993  elfz0ubfz0  13014  elfzo0z  13082  fzofzim  13087  ssfzoulel  13134  ssfzo12bi  13135  subfzo0  13162  modmuladdim  13285  modaddmodup  13305  modfzo0difsn  13314  axdc4uzlem  13354  expaddz  13476  sq01  13589  hashnn0n0nn  13755  hashss  13773  hashgt12el  13786  fi1uzind  13858  brfi1indALT  13861  ccatalpha  13949  swrdswrdlem  14068  swrdswrd  14069  swrdccatin1  14089  pfxccatin12lem3  14096  repswswrd  14148  cshf1  14174  cshw1  14186  2cshwcshw  14189  sqrmo  14613  caubnd2  14719  summo  15076  nno  15735  divalglem8  15753  lcmdvds  15954  lcmfunsnlem1  15983  hashgcdeq  16128  modprm0  16144  pcqcl  16195  vdwnnlem3  16335  prmgaplem5  16393  prmgaplem7  16395  catpropd  16981  cicsym  17076  isinitoi  17265  istermoi  17266  iszeroi  17271  acsfiindd  17789  tsrlemax  17832  issubg4  18300  gsmsymgreqlem2  18561  oddvdsnn0  18674  oddvds  18677  gexdvds  18711  lt6abl  19017  pgpfac1lem3  19201  coe1ae0  20386  isphld  20800  mdetdiaglem  21209  slesolex  21293  pmatcoe1fsupp  21311  cpmatelimp  21322  cpmatelimp2  21324  cpmatmcllem  21328  pm2mpf1  21409  mp2pm2mplem4  21419  fvmptnn04ifa  21460  fvmptnn04ifd  21463  chfacfscmul0  21468  chfacfpmmul0  21472  neii1  21716  neii2  21718  uncmp  22013  isfild  22468  fbunfip  22479  fgss2  22484  fgcl  22488  isufil2  22518  cfinufil  22538  ufilen  22540  fsumcn  23480  lmmbr  23863  iscau4  23884  caussi  23902  cmslssbn  23977  ovoliunnul  24110  ovolicc2lem4  24123  itg1ge0a  24314  rolle  24589  ulmcaulem  24984  cxpge0  25268  fsumvma  25791  gausslemma2dlem1a  25943  2sqb  26010  2sq2  26011  pntrsumbnd2  26145  pntlem3  26187  axeuclid  26751  axcontlem2  26753  usgrislfuspgr  26971  nbuhgr2vtx1edgblem  27135  usgredgsscusgredg  27243  upgrwlkvtxedg  27428  uspgr2wlkeq  27429  cyclnspth  27583  uspgrn2crct  27588  crctcshwlkn0lem4  27593  wlkiswwlks2lem5  27653  wlknewwlksn  27667  umgrwwlks2on  27738  clwwlkccatlem  27769  clwlkclwwlklem2a4  27777  clwlkclwwlklem2a  27778  clwwisshclwwslemlem  27793  clwwlkel  27827  wwlksubclwwlk  27839  clwwlknon1  27878  clwwlknonex2lem2  27889  uhgr3cyclexlem  27962  vdgn1frgrv3  28078  2wspmdisj  28118  frgrregord013  28176  spansncvi  29431  lnconi  29812  cdj3lem1  30213  metider  31136  prsrcmpltd  32349  gonar  32644  goalr  32646  satffunlem2lem1  32653  funeldmb  33008  nofv  33166  sltres  33171  finminlem  33668  clsint2  33679  bj-finsumval0  34569  finxpsuclem  34680  pibt2  34700  wl-exeq  34776  phpreu  34878  poimirlem26  34920  poimir  34927  ismtyima  35083  elpaddn0  36938  tendospcanN  38161  rexzrexnn0  39408  unxpwdom3  39702  fsovrfovd  40362  radcnvrat  40653  2reu8i  43319  zm1nn  43509  subsubelfzo0  43533  fzoopth  43534  2ffzoeq  43535  fargshiftf  43607  2pwp1prm  43758  lighneal  43783  isomuspgrlem1  43999  isassintop  44124  uzlidlring  44207  2zrngamgm  44217  ply1mulgsumlem1  44447  suppdm  44572  rrxsphere  44742  inlinecirc02plem  44780