Theorem impancom 456

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mo4  2600  spc2ed  3569  rexraleqim  3615  disjiun  5098  disjord  5099  disjiund  5101  propeqop  5488  euotd  5494  pwssun  5551  iotan0  6523  funopsn  7142  funopsnOLD  7143  isotr  7332  funeldmb  7355  resf1extb  7927  funfv1st2nd  8039  funelss  8040  el2mpocsbcl  8076  ressuppssdif  8177  oeordi  8569  domunsncan  9061  pssnn  9149  findcard3  9239  ordtypelem7  9482  inf3lem5  9597  r1tr  9744  cardmin2  9981  ac10ct  10014  isf32lem12  10344  isfin1-3  10366  fin17  10374  fin1a2s  10394  axdc4lem  10435  axcclem  10437  ttukeylem2  10490  genpcd  10987  ltexprlem3  11019  prlem936  11028  supsrlem  11092  mul0or  11850  un0addcl  12533  un0mulcl  12534  btwnnz  12668  uznfz  13634  elfz0ubfz0  13656  elfzo0z  13726  fzofzim  13734  ssfzoulel  13785  ssfzo12bi  13786  fzoopth  13787  subfzo0  13817  modmuladdim  13946  modaddmodup  13966  modfzo0difsn  13975  axdc4uzlem  14015  expaddz  14138  sq01  14257  hashnn0n0nn  14423  hashss  14441  hashgt12el  14455  fi1uzind  14540  brfi1indALT  14543  ccatalpha  14627  swrdswrdlem  14737  swrdswrd  14738  swrdccatin1  14758  pfxccatin12lem3  14765  repswswrd  14817  cshf1  14843  cshw1  14855  2cshwcshw  14858  sqrmo  15298  caubnd2  15405  summo  15764  nno  16436  divalglem8  16454  lcmdvds  16662  lcmfunsnlem1  16691  hashgcdeq  16845  modprm0  16861  pcqcl  16912  vdwnnlem3  17053  prmgaplem5  17111  prmgaplem7  17113  catpropd  17761  cicsym  17857  isinitoi  18052  istermoi  18053  iszeroi  18062  acsfiindd  18605  tsrlemax  18638  issubg4  19208  gsmsymgreqlem2  19497  oddvdsnn0  19610  oddvds  19613  gexdvds  19650  lt6abl  19961  pgpfac1lem3  20145  01eq0ring  20610  unichnlidl  21336  isphld  21769  psdmul  22294  coe1ae0  22341  mdetdiaglem  22720  slesolex  22804  pmatcoe1fsupp  22823  cpmatelimp  22834  cpmatelimp2  22836  cpmatmcllem  22840  pm2mpf1  22921  mp2pm2mplem4  22931  fvmptnn04ifa  22972  fvmptnn04ifd  22975  chfacfscmul0  22980  chfacfpmmul0  22984  neii1  23228  neii2  23230  uncmp  23525  isfild  23980  fbunfip  23991  fgss2  23996  fgcl  24000  isufil2  24030  cfinufil  24050  ufilen  24052  fsumcn  24994  lmmbr  25382  iscau4  25403  caussi  25421  cmslssbn  25496  ovoliunnul  25631  ovolicc2lem4  25644  itg1ge0a  25835  rolle  26114  ulmcaulem  26519  cxpge0  26810  fsumvma  27339  gausslemma2dlem1a  27491  2sqb  27558  2sq2  27559  pntrsumbnd2  27693  pntlem3  27735  nofv  27783  ltsres  27788  muls0ord  28340  axeuclid  29250  axcontlem2  29252  usgrislfuspgr  29474  nbuhgr2vtx1edgblem  29638  usgredgsscusgredg  29746  upgrwlkvtxedg  29931  uspgr2wlkeq  29932  cyclnspth  30087  uspgrn2crct  30094  crctcshwlkn0lem4  30099  wlkiswwlks2lem5  30159  wlknewwlksn  30173  usgrwwlks2on  30244  umgrwwlks2on  30245  clwwlkccatlem  30277  clwlkclwwlklem2a4  30285  clwlkclwwlklem2a  30286  clwwisshclwwslemlem  30301  clwwlkel  30334  wwlksubclwwlk  30346  clwwlknon1  30385  clwwlknonex2lem2  30396  uhgr3cyclexlem  30469  vdgn1frgrv3  30585  2wspmdisj  30625  frgrregord013  30683  spansncvi  31941  lnconi  32322  cdj3lem1  32723  constrsqrtcl  34110  metider  34225  prsrcmpltd  35410  onvf1odlem4  35485  gonar  35782  goalr  35784  satffunlem2lem1  35791  finminlem  36714  clsint2  36725  cgsex2gd  37664  bj-finsumval0  37812  finxpsuclem  37926  pibt2  37946  wl-exeq  38072  phpreu  38138  poimirlem26  38180  poimir  38187  ismtyima  38337  elpaddn0  40459  tendospcanN  41682  nnproddivdvdsd  42652  dvdsexpnn0  42978  sn-remul0ord  43052  rexzrexnn0  43416  unxpwdom3  43707  unielss  43830  onov0suclim  43886  fsovrfovd  44620  radcnvrat  44909  2reu8i  47732  zm1nn  47921  subsubelfzo0  47946  2ffzoeq  47947  nnmul2  47949  fargshiftf  48071  2pwp1prm  48223  lighneal  48245  isuspgrimlem  48542  upgrimpths  48556  clnbgr3stgrgrlim  48666  gpgedgvtx0  48708  gpgedgvtx1  48709  isassintop  48857  uzlidlring  48882  2zrngamgm  48892  ply1mulgsumlem1  49044  suppdm  49168  rrxsphere  49406  inlinecirc02plem  49444  pgindnf  50372