Theorem expd 421

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.)

Hypothesis

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

Assertion

Ref	Expression
expd	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem expd

Step	Hyp	Ref	Expression
1		expd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expdcom 420	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 88	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:  expcomd  422  exp32  426  exp4b  436  exp4c  438  exp4d  439  exp42  441  exp44  443  exp5c  450  exp5j  451  exp5l  452  pm3.3  454  expdimp  458  impl  461  syland  615  mpan2d  707  a2and  859  3impib  1134  exp5o  1374  ralrimivv  3205  mob2  3676  reuind  3714  reupick3  4279  elpwunsn  4648  disjiun  5095  sotr2  5601  wefrc  5653  relop  5834  predpoirr  6335  predfrirr  6336  fnun  6650  mpteqb  7010  tpres  7204  fconst5  7209  funfvima  7233  riotaeqimp  7400  dfwe2  7777  limuni3  7852  tfisi  7859  trom  7875  funcnvuni  7933  resf1ext2b  7936  f1oweALT  7973  frxp  8128  poxp  8130  poxp2  8145  poxp3  8152  wfr3g  8322  onfununi  8334  tz7.48lem  8434  oecl  8528  oaordex  8549  oaass  8552  omwordri  8563  odi  8570  omass  8571  omeu  8576  oen0  8578  oewordi  8583  oewordri  8584  nnarcl  8608  nnmass  8616  brinxper  8730  findcard2  9163  rex2dom  9227  dif1ennnALT  9251  unblem1  9266  unblem2  9267  domunfican  9295  marypha1lem  9407  supiso  9450  inf3lem3  9613  epfrs  9714  frr3g  9742  kardenOLD  9903  infxpenlem  10020  iunfictbso  10121  dfac5  10135  dfac2b  10137  kmlem1  10157  kmlem9  10165  infpssrlem3  10311  fin23lem25  10330  fin23lem30  10348  domtriomlem  10448  axdc3lem4  10459  axcclem  10463  zorn2lem7  10508  konigthlem  10581  wunr1om  10732  tskr1om  10780  gruen  10825  grur1a  10832  indpi  10920  genpnmax  11020  prlem934  11046  ltaddpr  11047  ltexprlem7  11055  ltaprlem  11057  axrrecex  11176  axpre-sup  11182  lelttr  11328  dedekind  11401  addlid  11421  nn0lt2  12688  fzind  12723  fnn0ind  12724  btwnz  12728  uzwo  12964  lbzbi  12989  rpnnen1lem5  13035  ledivge1le  13119  xrlelttr  13211  qbtwnre  13255  xrsupsslem  13363  xrinfmsslem  13364  supxrun  13372  elfz1b  13652  elfz0ubfz0  13691  elfzo0z  13761  fzofzim  13769  elfznelfzo  13833  fleqceilz  13919  fsequb  14043  leexp2r  14242  bernneq  14297  fi1uzind  14576  brfi1indALT  14579  swrdnd0  14731  swrdswrdlem  14777  swrdswrd  14778  wrd2ind  14796  swrdccatin1  14798  swrdccatin2  14802  pfxccatin12lem3  14805  repswswrd  14859  cshweqrep  14896  swrd2lsw  15029  2swrd2eqwrdeq  15030  wrdl3s3  15039  s3iunsndisj  15045  cau3lem  15446  climuni  15643  mulcn2  15687  dvdsabseq  16409  divalglem8  16496  ndvdssub  16505  rplpwr  16654  algcvgblem  16673  lcmf  16729  lcmftp  16732  lcmfunsnlem2lem1  16734  lcmfunsnlem2lem2  16735  lcmfdvdsb  16739  lcmfun  16741  euclemma  16810  prmlem1a  17204  setsstruct2  17272  iscatd  17767  initoeu1  18106  initoeu2  18111  termoeu1  18113  plelttr  18436  insubm  18933  grpinveu  19104  cyccom  19337  symgfixelsi  19568  efgred  19881  telgsumfzs  20122  srgmulgass  20362  srgbinom  20376  lspdisjb  21319  mplcoe5lem  22261  cply1mul  22527  coe1fzgsumd  22535  gsummoncoe1  22539  evl1gsumd  22588  cpmatacl  22947  cpmatmcllem  22949  basis2  23182  0ntr  23302  uncmp  23634  1stcrest  23684  txcls  23836  txcnp  23852  tx1stc  23882  fgss2  24106  alexsubALTlem2  24280  alexsubALTlem3  24281  alexsubALTlem4  24282  metcnp3  24772  tngngp3  24888  reconn  25061  iscau4  25513  ellimc3  26113  ulmbdd  26641  ulmcn  26642  sinq12ge0  26753  gausslemma2dlem3  27612  2sq2  27677  2sqreultlem  27691  2sqreunnltlem  27694  sltsleft  28133  sltsright  28134  noseqind  28565  oldfib  28650  expsgt0  28710  bdayfinbndlem1  28740  bdayfin  28760  elreno2  28768  ax5seglem5  29398  ax5seg  29403  uhgrnbgr0nb  29822  cplgrop  29905  wlkl1loop  30105  uspgr2wlkeq  30113  upgrwlkdvdelem  30209  uhgrwkspthlem2  30227  pthdlem2lem  30240  uspgrn2crct  30284  wlkiswwlks2lem3  30347  wlkiswwlks2  30351  wlkiswwlksupgr2  30353  wlklnwwlkln2lem  30358  wwlksnext  30369  wwlksnextfun  30374  rusgrnumwwlk  30454  clwlkclwwlklem2a4  30475  clwlkclwwlklem3  30479  erclwwlksym  30499  erclwwlknsym  30548  eleclclwwlkn  30554  clwwlknonwwlknonb  30584  umgr2cycllem  30633  umgr2cycl  30634  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  conngrv2edg  30683  eupth2lem3lem6  30721  frgrncvvdeqlem8  30794  frgrwopreglem4a  30798  frgrreggt1  30881  frgrreg  30882  grpoinveu  31008  ococss  31782  shmodsi  31878  h1datomi  32070  hoaddsub  32305  adjmul  32581  chjatom  32846  atomli  32871  atcvat4i  32886  mdsymlem3  32894  mdsymlem5  32896  mdsymlem6  32897  sumdmdlem  32907  cdj3lem2a  32925  cdj3lem3a  32928  bnj1204  35529  fineqvinfep  35659  cvmsdisj  35857  satfv0fun  35958  satffunlem  35988  satffunlem1lem2  35990  satffunlem2lem2  35993  fundmpss  36354  dfon2lem6  36373  dfon2lem8  36375  ifscgr  36632  lineext  36664  fscgr  36668  idinside  36672  btwnconn1lem11  36685  btwnconn1lem12  36686  btwnconn3  36691  brsegle  36696  seglecgr12  36699  hilbert1.2  36743  exp5d  36930  exp5k  36932  nn0prpwlem  36949  mh-inf3f1  37168  bj-restb  37852  exrecfnlem  38141  poimirlem26  38403  poimirlem29  38406  poimirlem32  38409  areacirc  38470  heibor1lem  38567  pridl  38795  pridlc  38829  dmnnzd  38833  disjlem17  39658  membpartlem19  39670  prtlem11  39747  prtlem17  39757  ax12indn  39824  atcvrj0  40309  cvrat4  40324  athgt  40337  lplnexllnN  40445  2llnjN  40448  lvolnle3at  40463  lncmp  40664  paddclN  40723  pexmidlem4N  40854  cdleme17d3  41377  cdleme50trn2  41432  cdlemf2  41443  cdlemf  41444  cdlemj3  41704  cdlemk26b-3  41786  dihord5b  42140  isnacs3  43563  jm2.26  43851  ordnexbtwnsuc  44116  omabs2  44181  naddgeoa  44243  sbiota1  45266  exbir  45310  tratrb  45367  onfrALT  45380  in2an  45439  pwtrrVD  45655  suctrALT2VD  45666  suctrALT2  45667  tratrbVD  45691  trintALTVD  45710  trintALT  45711  or2expropbi  47930  fcoresf1  47965  2reu8i  48009  2reuimp  48011  zm1nn  48198  2ffzoeq  48224  iccpartiltu  48330  iccpartigtl  48331  iccpartgt  48335  iccpartnel  48346  sbcpr  48429  fmtnofac2lem  48479  fmtnofac2  48480  lighneallem2  48517  odd2prm2  48642  stgoldbwt  48700  sbgoldbst  48702  sbgoldbaltlem1  48703  mogoldbb  48709  uhgrimisgrgric  48855  clnbgrgrim  48858  grimedg  48859  gpgedgvtx1  48986  gpgedg2iv  48991  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem6  49048  pgnbgreunbgr  49049  lidldomn1  49154  idomnzd  49269  ply1mulgsumlem1  49324  lincsumcl  49369  ellcoellss  49373  islinindfis  49387  lindslinindsimp1  49395  lindslinindsimp2lem5  49400  lindsrng01  49406  elfzolborelfzop1  49457  rrx2linest  49680  aacllem  50780