Theorem impd 412

Description: Importation deduction. (Contributed by NM, 31-Mar-1994.)

Hypothesis

Ref	Expression
impd.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
impd	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem impd

Step	Hyp	Ref	Expression
1		impd.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2	1	com3l 89	. . 3 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	imp 408	. 2 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜃))
4	3	com12 32	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  impcomd  413  imp32  420  imp4b  423  imp4c  425  imp4d  426  imp5d  441  imp5g  443  pm3.31  451  expimpd  455  expl  459  ancomsd  467  syland  604  3expib  1123  ax13lem1  2374  equs5  2460  rsp2  3275  moi  3714  reu6  3722  sbciegft  3815  ss2abdv  4060  elpwunsn  4687  opthpr  4852  preqsnd  4859  opthprneg  4865  3elpr2eq  4907  invdisj  5132  snopeqop  5506  solin  5613  sotr2  5620  wefrc  5670  relop  5849  elinxp  6018  reuop  6290  dfpo2  6293  tz7.7  6388  ordtr2  6406  funopsn  7143  tpres  7199  funfvima  7229  isomin  7331  sorpsscmpl  7721  peano5  7881  peano5OLD  7882  f1oweALT  7956  poxp  8111  soxp  8112  tfr3  8396  tz7.48-1  8440  omordi  8563  odi  8576  omass  8577  oen0  8583  nndi  8620  nnmass  8621  nnmordi  8628  eroveu  8803  ssfi  9170  findcard3  9282  findcard3OLD  9283  fiint  9321  suplub  9452  hartogs  9536  card2on  9546  unxpwdom2  9580  inf3lem2  9621  ttrclselem2  9718  epfrs  9723  tcel  9737  frr3g  9748  dfac2b  10122  infpssr  10300  isf32lem9  10353  axdc3lem4  10445  axcclem  10449  zorn2lem7  10494  ttukeylem6  10506  brdom6disj  10524  ondomon  10555  inar1  10767  gruen  10804  indpi  10899  nqereu  10921  genpn0  10995  distrlem1pr  11017  distrlem5pr  11019  ltexprlem1  11028  reclem4pr  11042  addsrmo  11065  mulsrmo  11066  supsrlem  11103  lelttr  11301  ltlen  11312  mulgt1  12070  fzind  12657  xrlelttr  13132  xnn0xaddcl  13211  fzen  13515  bernneq  14189  swrdswrdlem  14651  repsdf2  14725  limsupbnd2  15424  mulcn2  15537  prodmolem2  15876  dvdsmod0  16200  lcmfunsnlem1  16571  divgcdcoprm0  16599  maxprmfct  16643  pceu  16776  dvdsprmpweqnn  16815  oddprmdvds  16833  infpnlem1  16840  prmgaplem6  16986  imasaddfnlem  17471  initoeu1  17958  termoeu1  17965  plelttr  18294  gsumval2a  18601  cycsubm  19074  symgfix2  19279  psgnunilem4  19360  lsmmod  19538  efgrelexlemb  19613  imasabl  19739  pgpfac1lem5  19944  lindfrn  21368  mat1dimcrng  21971  dmatelnd  21990  mdetunilem7  22112  cpmatacl  22210  cpmatmcllem  22212  lmss  22794  hausnei2  22849  isnrm2  22854  isnrm3  22855  cmpsublem  22895  2ndcdisj  22952  txcnpi  23104  tx1stc  23146  fgcl  23374  ufileu  23415  fmfnfmlem4  23453  fmfnfm  23454  alexsubALTlem4  23546  alexsubALT  23547  tmdgsum2  23592  prdsxmslem2  24030  ovolicc2  25031  volfiniun  25056  dyadmax  25107  ellimc3  25388  dvlip2  25504  dvne0  25520  zabsle1  26789  2lgslem3  26897  2sqreulem3  26946  scutun12  27301  mulsproplem9  27570  mulsprop  27576  axcontlem4  28215  uhgr2edg  28455  ushgredgedg  28476  ushgredgedgloop  28478  nb3grprlem1  28627  rusgr1vtx  28835  wlkonl1iedg  28912  uhgrwkspthlem2  29001  usgr2wlkneq  29003  usgr2trlncl  29007  uspgrn2crct  29052  wspthsnonn0vne  29161  umgrwwlks2on  29201  elwspths2on  29204  clwlkclwwlkf1lem3  29249  erclwwlktr  29265  erclwwlkntr  29314  frgrnbnb  29536  frgr2wwlk1  29572  frrusgrord  29584  wlkl0  29610  isch3  30482  ocin  30537  shmodsi  30630  spansneleq  30811  stj  31476  atom1d  31594  atcvat2i  31628  chirredlem1  31631  chirredi  31635  mdsymlem3  31646  mdsymlem6  31649  bnj849  33925  pconnconn  34211  cvmsss2  34254  cvmliftlem7  34271  satfv0  34338  satfv0fun  34351  satffunlem  34381  satffunlem1lem1  34382  satffunlem2lem1  34384  mclsind  34550  dfon2lem9  34752  dfon2  34753  cgrextend  34969  btwntriv2  34973  btwncomim  34974  btwnexch3  34981  funtransport  34992  ifscgr  35005  colinearxfr  35036  lineext  35037  fscgr  35041  outsideoftr  35090  gg-dvfsumlem2  35172  trer  35190  finminlem  35192  fnessref  35231  fgmin  35244  bj-andnotim  35455  bj-alanim  35479  bj-0int  35971  relowlssretop  36233  finorwe  36252  finxpsuclem  36267  wl-ax13lem1  36364  poimirlem29  36506  itg2addnclem3  36530  itg2addnc  36531  areacirc  36570  ismtybndlem  36663  heibor1lem  36666  iss2  37202  disjlem17  37658  membpartlem19  37670  prtlem17  37735  riotasvd  37815  lshpsmreu  37968  atnle  38176  cvratlem  38281  cvrat2  38289  3dim1  38327  2llnjN  38427  2lplnj  38480  linepsubN  38612  pmapsub  38628  paddasslem14  38693  pclfinN  38760  ispsubcl2N  38807  pclfinclN  38810  ldilval  38973  trlord  39429  cdlemk36  39773  dihlsscpre  40094  baerlem3lem2  40570  baerlem5alem2  40571  baerlem5blem2  40572  pellexlem5  41557  pellex  41559  pell1234qrmulcl  41579  pellfundex  41610  cantnfresb  42060  omabs2  42068  relexpmulnn  42446  clsk1indlem3  42780  19.41rg  43297  iunconnlem2  43682  or2expropbi  45731  fcoresf1  45766  euoreqb  45804  2reu8i  45808  dfatcolem  45950  f1oresf1o2  45986  nltle2tri  46008  imasetpreimafvbijlemf1  46059  iccpartnel  46093  ich2exprop  46126  ichreuopeq  46128  paireqne  46166  prprelprb  46172  reupr  46177  reuopreuprim  46181  fmtnofac2lem  46223  sfprmdvdsmersenne  46258  lighneallem3  46262  lighneallem4  46265  requad2  46278  bgoldbtbnd  46464  isomuspgrlem2d  46486  isomgrsym  46491  isomgrtr  46494  upgrwlkupwlk  46505  rngqiprngimf1lem  46760  rngqiprngimfo  46767  nzerooringczr  46924  ldepspr  47108  affinecomb1  47342  itsclc0  47411  aacllem  47802