Theorem impancom 457

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mo4  2591  spc2ed  3555  rexraleqim  3600  prsrcmpltd  4432  disjiun  5090  disjord  5091  disjiund  5093  propeqop  5478  euotd  5485  pwssun  5542  iotan0  6528  iotan0OLD  6529  funopsn  7152  funopsnOLD  7153  isotr  7345  funeldmb  7370  resf1extb  7947  funfv1st2nd  8058  funelss  8059  el2mpocsbcl  8097  ressuppssdif  8206  oeordi  8600  domunsncan  9100  pssnn  9188  findcard3  9278  ordtypelem7  9522  inf3lem5  9637  r1tr  9787  cardmin2  10084  ac10ct  10117  isf32lem12  10446  isfin1-3  10468  fin17  10476  fin1a2s  10496  axdc4lem  10537  axcclem  10539  ttukeylem2  10592  genpcd  11095  ltexprlem3  11127  prlem936  11136  supsrlem  11200  mul0or  11960  un0addcl  12643  un0mulcl  12644  btwnnz  12779  uznfz  13748  elfz0ubfz0  13770  elfzo0z  13840  fzofzim  13848  ssfzoulel  13899  ssfzo12bi  13900  fzoopth  13901  subfzo0  13932  modmuladdim  14061  modaddmodup  14081  modfzo0difsn  14090  axdc4uzlem  14130  expaddz  14253  sq01  14373  hashnn0n0nn  14539  hashss  14557  hashgt12el  14571  fi1uzind  14656  brfi1indALT  14659  ccatalpha  14744  swrdswrdlem  14858  swrdswrd  14859  swrdccatin1  14879  pfxccatin12lem3  14886  repswswrd  14940  cshf1  14966  cshw1  14978  2cshwcshw  14981  sqrmo  15424  caubnd2  15531  summo  15889  nno  16558  divalglem8  16576  lcmdvds  16789  lcmfunsnlem1  16818  hashgcdeq  16973  modprm0  16989  pcqcl  17040  vdwnnlem3  17181  prmgaplem5  17239  prmgaplem7  17241  catpropd  17889  cicsym  17985  isinitoi  18180  istermoi  18181  iszeroi  18190  acsfiindd  18733  tsrlemax  18766  0gisid  18854  issubg4  19362  gsmsymgreqlem2  19651  oddvdsnn0  19764  oddvds  19767  gexdvds  19804  lt6abl  20115  pgpfac1lem3  20299  01eq0ring  20787  unichnlidl  21522  isphld  21966  psdmul  22493  coe1ae0  22540  mdetdiaglem  22919  slesolex  23006  pmatcoe1fsupp  23025  cpmatelimp  23036  cpmatelimp2  23038  cpmatmcllem  23042  pm2mpf1  23123  mp2pm2mplem4  23133  fvmptnn04ifa  23174  fvmptnn04ifd  23177  chfacfscmul0  23182  chfacfpmmul0  23186  neii1  23430  neii2  23432  uncmp  23727  isfild  24183  fbunfip  24194  fgss2  24199  fgcl  24203  isufil2  24233  cfinufil  24253  ufilen  24255  fsumcn  25197  lmmbr  25585  iscau4  25606  caussi  25624  cmslssbn  25699  ovoliunnul  25834  ovolicc2lem4  25847  itg1ge0a  26038  rolle  26316  ulmcaulem  26727  cxpge0  27017  fsumvma  27546  gausslemma2dlem1a  27698  2sqb  27765  2sq2  27766  pntrsumbnd2  27900  pntlem3  27942  nofv  28020  ltsres  28025  muls0ord  28577  axeuclid  29547  axcontlem2  29549  usgrislfuspgr  29774  nbuhgr2vtx1edgblem  29938  usgredgsscusgredg  30046  upgrwlkvtxedg  30231  uspgr2wlkeq  30232  cyclnspth  30395  uspgrn2crct  30403  crctcshwlkn0lem4  30408  wlkiswwlks2lem5  30468  wlknewwlksn  30482  usgrwwlks2on  30553  umgrwwlks2on  30554  clwwlkccatlem  30586  clwlkclwwlklem2a4  30594  clwlkclwwlklem2a  30595  clwwisshclwwslemlem  30610  clwwlkel  30643  wwlksubclwwlk  30655  clwwlknon1  30694  clwwlknonex2lem2  30705  uhgr3cyclexlem  30788  vdgn1frgrv3  30904  2wspmdisj  30944  frgrregord013  31002  spansncvi  32260  lnconi  32641  cdj3lem1  33042  constrsqrtcl  34458  metider  34573  onvf1odlem4  35954  onprcf1acwevdlem1  35965  gonar  36247  goalr  36249  satffunlem2lem1  36256  mirimanoffr  36547  finminlem  37199  clsint2  37210  cgsex2gd  38152  bj-finsumval0  38300  finxpsuclem  38414  pibt2  38434  wl-exeq  38560  phpreu  38621  poimirlem26  38658  poimir  38665  ismtyima  38831  elpaddn0  40951  tendospcanN  42174  nnproddivdvdsd  43144  dvdsexpnn0  43480  sn-remul0ord  43553  rexzrexnn0  43905  unxpwdom3  44191  unielss  44314  onov0suclim  44370  fsovrfovd  45103  radcnvrat  45392  2reu8i  48277  zm1nn  48466  subsubelfzo0  48491  2ffzoeq  48492  nnmul2  48494  fargshiftf  48616  2pwp1prm  48768  lighneal  48790  isuspgrimlem  49087  upgrimpths  49101  clnbgr3stgrgrlim  49211  gpgedgvtx0  49253  gpgedgvtx1  49254  isassintop  49401  uzlidlring  49426  2zrngamgm  49436  ply1mulgsumlem1  49592  suppdm  49716  rrxsphere  49954  inlinecirc02plem  49992  pgindnf  50978