Theorem impancom 452

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mo4  2567  eqrdav  2738  spc2ed  3541  rexraleqim  3578  disjiun  5062  disjord  5063  disjiund  5065  propeqop  5422  euotd  5428  pwssun  5486  iotan0  6427  funopsn  7029  isotr  7216  funfv1st2nd  7896  funelss  7897  el2mpocsbcl  7934  ressuppssdif  8010  oeordi  8427  domunsncan  8868  pssnn  8960  pssnnOLD  9049  findcard3  9066  ordtypelem7  9292  inf3lem5  9399  r1tr  9543  cardmin2  9766  ac10ct  9799  isf32lem12  10129  isfin1-3  10151  fin17  10159  fin1a2s  10179  axdc4lem  10220  axcclem  10222  ttukeylem2  10275  genpcd  10771  ltexprlem3  10803  prlem936  10812  supsrlem  10876  mul0or  11624  un0addcl  12275  un0mulcl  12276  btwnnz  12405  uznfz  13348  elfz0ubfz0  13369  elfzo0z  13438  fzofzim  13443  ssfzoulel  13490  ssfzo12bi  13491  subfzo0  13518  modmuladdim  13643  modaddmodup  13663  modfzo0difsn  13672  axdc4uzlem  13712  expaddz  13836  sq01  13949  hashnn0n0nn  14115  hashss  14133  hashgt12el  14146  fi1uzind  14220  brfi1indALT  14223  ccatalpha  14307  swrdswrdlem  14426  swrdswrd  14427  swrdccatin1  14447  pfxccatin12lem3  14454  repswswrd  14506  cshf1  14532  cshw1  14544  2cshwcshw  14547  sqrmo  14972  caubnd2  15078  summo  15438  nno  16100  divalglem8  16118  lcmdvds  16322  lcmfunsnlem1  16351  hashgcdeq  16499  modprm0  16515  pcqcl  16566  vdwnnlem3  16707  prmgaplem5  16765  prmgaplem7  16767  catpropd  17427  cicsym  17525  isinitoi  17723  istermoi  17724  iszeroi  17733  acsfiindd  18280  tsrlemax  18313  issubg4  18783  gsmsymgreqlem2  19048  oddvdsnn0  19161  oddvds  19164  gexdvds  19198  lt6abl  19505  pgpfac1lem3  19689  isphld  20868  coe1ae0  21396  mdetdiaglem  21756  slesolex  21840  pmatcoe1fsupp  21859  cpmatelimp  21870  cpmatelimp2  21872  cpmatmcllem  21876  pm2mpf1  21957  mp2pm2mplem4  21967  fvmptnn04ifa  22008  fvmptnn04ifd  22011  chfacfscmul0  22016  chfacfpmmul0  22020  neii1  22266  neii2  22268  uncmp  22563  isfild  23018  fbunfip  23029  fgss2  23034  fgcl  23038  isufil2  23068  cfinufil  23088  ufilen  23090  fsumcn  24042  lmmbr  24431  iscau4  24452  caussi  24470  cmslssbn  24545  ovoliunnul  24680  ovolicc2lem4  24693  itg1ge0a  24885  rolle  25163  ulmcaulem  25562  cxpge0  25847  fsumvma  26370  gausslemma2dlem1a  26522  2sqb  26589  2sq2  26590  pntrsumbnd2  26724  pntlem3  26766  axeuclid  27340  axcontlem2  27342  usgrislfuspgr  27563  nbuhgr2vtx1edgblem  27727  usgredgsscusgredg  27835  upgrwlkvtxedg  28021  uspgr2wlkeq  28022  cyclnspth  28177  uspgrn2crct  28182  crctcshwlkn0lem4  28187  wlkiswwlks2lem5  28247  wlknewwlksn  28261  umgrwwlks2on  28331  clwwlkccatlem  28362  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwwisshclwwslemlem  28386  clwwlkel  28419  wwlksubclwwlk  28431  clwwlknon1  28470  clwwlknonex2lem2  28481  uhgr3cyclexlem  28554  vdgn1frgrv3  28670  2wspmdisj  28710  frgrregord013  28768  spansncvi  30023  lnconi  30404  cdj3lem1  30805  metider  31853  prsrcmpltd  33064  gonar  33366  goalr  33368  satffunlem2lem1  33375  funeldmb  33746  nofv  33869  sltres  33874  finminlem  34516  clsint2  34527  bj-finsumval0  35465  finxpsuclem  35577  pibt2  35597  wl-exeq  35702  phpreu  35770  poimirlem26  35812  poimir  35819  ismtyima  35970  elpaddn0  37821  tendospcanN  39044  nnproddivdvdsd  40016  dvdsexpnn0  40348  rexzrexnn0  40633  unxpwdom3  40927  fsovrfovd  41624  radcnvrat  41939  2reu8i  44616  zm1nn  44805  subsubelfzo0  44829  fzoopth  44830  2ffzoeq  44831  fargshiftf  44903  2pwp1prm  45052  lighneal  45074  isomuspgrlem1  45290  isassintop  45415  uzlidlring  45498  2zrngamgm  45508  ply1mulgsumlem1  45738  suppdm  45862  rrxsphere  46105  inlinecirc02plem  46143