Theorem impancom 450

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mo4  2554  eqrdav  2724  spc2ed  3585  rexraleqim  3630  disjiun  5136  disjord  5137  disjiund  5139  propeqop  5509  euotd  5515  pwssun  5573  iotan0  6539  funopsn  7157  isotr  7343  funeldmb  7366  funfv1st2nd  8051  funelss  8052  el2mpocsbcl  8090  ressuppssdif  8190  oeordi  8608  domunsncan  9097  pssnn  9193  pssnnOLD  9290  findcard3  9310  findcard3OLD  9311  ordtypelem7  9549  inf3lem5  9657  r1tr  9801  cardmin2  10024  ac10ct  10059  isf32lem12  10389  isfin1-3  10411  fin17  10419  fin1a2s  10439  axdc4lem  10480  axcclem  10482  ttukeylem2  10535  genpcd  11031  ltexprlem3  11063  prlem936  11072  supsrlem  11136  mul0or  11886  un0addcl  12538  un0mulcl  12539  btwnnz  12671  uznfz  13619  elfz0ubfz0  13640  elfzo0z  13709  fzofzim  13714  ssfzoulel  13761  ssfzo12bi  13762  fzoopth  13763  subfzo0  13790  modmuladdim  13915  modaddmodup  13935  modfzo0difsn  13944  axdc4uzlem  13984  expaddz  14107  sq01  14223  hashnn0n0nn  14386  hashss  14404  hashgt12el  14417  fi1uzind  14494  brfi1indALT  14497  ccatalpha  14579  swrdswrdlem  14690  swrdswrd  14691  swrdccatin1  14711  pfxccatin12lem3  14718  repswswrd  14770  cshf1  14796  cshw1  14808  2cshwcshw  14812  sqrmo  15234  caubnd2  15340  summo  15699  nno  16362  divalglem8  16380  lcmdvds  16582  lcmfunsnlem1  16611  hashgcdeq  16761  modprm0  16777  pcqcl  16828  vdwnnlem3  16969  prmgaplem5  17027  prmgaplem7  17029  catpropd  17692  cicsym  17790  isinitoi  17991  istermoi  17992  iszeroi  18001  acsfiindd  18548  tsrlemax  18581  issubg4  19108  gsmsymgreqlem2  19398  oddvdsnn0  19511  oddvds  19514  gexdvds  19551  lt6abl  19862  pgpfac1lem3  20046  01eq0ring  20479  isphld  21603  psdmul  22113  coe1ae0  22159  mdetdiaglem  22544  slesolex  22628  pmatcoe1fsupp  22647  cpmatelimp  22658  cpmatelimp2  22660  cpmatmcllem  22664  pm2mpf1  22745  mp2pm2mplem4  22755  fvmptnn04ifa  22796  fvmptnn04ifd  22799  chfacfscmul0  22804  chfacfpmmul0  22808  neii1  23054  neii2  23056  uncmp  23351  isfild  23806  fbunfip  23817  fgss2  23822  fgcl  23826  isufil2  23856  cfinufil  23876  ufilen  23878  fsumcn  24832  lmmbr  25230  iscau4  25251  caussi  25269  cmslssbn  25344  ovoliunnul  25480  ovolicc2lem4  25493  itg1ge0a  25685  rolle  25966  ulmcaulem  26375  cxpge0  26662  fsumvma  27191  gausslemma2dlem1a  27343  2sqb  27410  2sq2  27411  pntrsumbnd2  27545  pntlem3  27587  nofv  27636  sltres  27641  muls0ord  28135  axeuclid  28846  axcontlem2  28848  usgrislfuspgr  29072  nbuhgr2vtx1edgblem  29236  usgredgsscusgredg  29345  upgrwlkvtxedg  29531  uspgr2wlkeq  29532  cyclnspth  29686  uspgrn2crct  29691  crctcshwlkn0lem4  29696  wlkiswwlks2lem5  29756  wlknewwlksn  29770  umgrwwlks2on  29840  clwwlkccatlem  29871  clwlkclwwlklem2a4  29879  clwlkclwwlklem2a  29880  clwwisshclwwslemlem  29895  clwwlkel  29928  wwlksubclwwlk  29940  clwwlknon1  29979  clwwlknonex2lem2  29990  uhgr3cyclexlem  30063  vdgn1frgrv3  30179  2wspmdisj  30219  frgrregord013  30277  spansncvi  31534  lnconi  31915  cdj3lem1  32316  metider  33623  prsrcmpltd  34834  gonar  35133  goalr  35135  satffunlem2lem1  35142  finminlem  35930  clsint2  35941  bj-finsumval0  36892  finxpsuclem  37004  pibt2  37024  wl-exeq  37129  phpreu  37205  poimirlem26  37247  poimir  37254  ismtyima  37404  elpaddn0  39400  tendospcanN  40623  nnproddivdvdsd  41600  dvdsexpnn0  42033  rexzrexnn0  42363  unxpwdom3  42658  unielss  42785  onov0suclim  42842  fsovrfovd  43578  radcnvrat  43890  2reu8i  46628  zm1nn  46817  subsubelfzo0  46841  2ffzoeq  46842  fargshiftf  46914  2pwp1prm  47063  lighneal  47085  isuspgrimlem  47355  isassintop  47455  uzlidlring  47480  2zrngamgm  47490  ply1mulgsumlem1  47637  suppdm  47761  rrxsphere  48004  inlinecirc02plem  48042  pgindnf  48330