Theorem expd 420

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 419	. 2 ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃)))
3	2	com3r 88	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  expcomd  421  exp32  425  exp4b  435  exp4c  437  exp4d  438  exp42  440  exp44  442  exp5c  449  exp5j  450  exp5l  451  pm3.3  453  expdimp  457  impl  460  syland  614  mpan2d  706  a2and  858  3impib  1134  exp5o  1374  ralrimivv  3206  mob2  3679  reuind  3717  reupick3  4284  elpwunsn  4651  disjiun  5098  sotr2  5605  wefrc  5657  relop  5838  predpoirr  6336  predfrirr  6337  fnun  6651  mpteqb  7011  tpres  7201  fconst5  7206  funfvima  7230  riotaeqimp  7395  dfwe2  7774  limuni3  7849  tfisi  7856  trom  7872  funcnvuni  7930  resf1ext2b  7933  f1oweALT  7970  frxp  8123  poxp  8125  poxp2  8140  poxp3  8147  wfr3g  8317  onfununi  8329  tz7.48lem  8429  oecl  8523  oaordex  8544  oaass  8547  omwordri  8558  odi  8565  omass  8566  omeu  8571  oen0  8573  oewordi  8578  oewordri  8579  nnarcl  8603  nnmass  8611  brinxper  8725  findcard2  9150  rex2dom  9214  dif1ennnALT  9238  unblem1  9253  unblem2  9254  domunfican  9282  marypha1lem  9394  supiso  9437  inf3lem3  9600  epfrs  9701  frr3g  9729  karden  9882  infxpenlem  9998  iunfictbso  10099  dfac5  10113  dfac2b  10115  kmlem1  10135  kmlem9  10143  infpssrlem3  10290  fin23lem25  10309  fin23lem30  10327  domtriomlem  10427  axdc3lem4  10438  axcclem  10442  zorn2lem7  10487  konigthlem  10554  wunr1om  10705  tskr1om  10753  gruen  10798  grur1a  10805  indpi  10893  genpnmax  10993  prlem934  11019  ltaddpr  11020  ltexprlem7  11028  ltaprlem  11030  axrrecex  11149  axpre-sup  11155  lelttr  11301  dedekind  11374  addlid  11394  nn0lt2  12660  fzind  12695  fnn0ind  12696  btwnz  12700  uzwo  12936  lbzbi  12961  rpnnen1lem5  13006  ledivge1le  13090  xrlelttr  13182  qbtwnre  13226  xrsupsslem  13334  xrinfmsslem  13335  supxrun  13343  elfz1b  13623  elfz0ubfz0  13662  elfzo0z  13732  fzofzim  13740  elfznelfzo  13804  fleqceilz  13889  fsequb  14013  leexp2r  14212  bernneq  14267  fi1uzind  14546  brfi1indALT  14549  swrdnd0  14697  swrdswrdlem  14743  swrdswrd  14744  wrd2ind  14762  swrdccatin1  14764  swrdccatin2  14768  pfxccatin12lem3  14771  repswswrd  14823  cshweqrep  14860  swrd2lsw  14991  2swrd2eqwrdeq  14992  wrdl3s3  15001  s3iunsndisj  15007  cau3lem  15408  climuni  15605  mulcn2  15649  dvdsabseq  16372  divalglem8  16459  ndvdssub  16468  rplpwr  16617  algcvgblem  16636  lcmf  16692  lcmftp  16695  lcmfunsnlem2lem1  16697  lcmfunsnlem2lem2  16698  lcmfdvdsb  16702  lcmfun  16704  euclemma  16773  prmlem1a  17167  setsstruct2  17235  iscatd  17730  initoeu1  18069  initoeu2  18074  termoeu1  18076  plelttr  18399  insubm  18878  grpinveu  19042  cyccom  19275  symgfixelsi  19506  efgred  19819  telgsumfzs  20060  srgmulgass  20300  srgbinom  20314  lspdisjb  21231  mplcoe5lem  22171  cply1mul  22437  coe1fzgsumd  22445  gsummoncoe1  22449  evl1gsumd  22498  cpmatacl  22854  cpmatmcllem  22856  basis2  23089  0ntr  23209  uncmp  23541  1stcrest  23591  txcls  23742  txcnp  23758  tx1stc  23788  fgss2  24012  alexsubALTlem2  24186  alexsubALTlem3  24187  alexsubALTlem4  24188  metcnp3  24678  tngngp3  24794  reconn  24967  iscau4  25419  ellimc3  26019  ulmbdd  26539  ulmcn  26540  sinq12ge0  26651  gausslemma2dlem3  27510  2sq2  27575  2sqreultlem  27589  2sqreunnltlem  27592  sltsleft  28031  sltsright  28032  noseqind  28463  oldfib  28548  expsgt0  28608  bdayfinbndlem1  28638  bdayfin  28658  elreno2  28666  ax5seglem5  29261  ax5seg  29266  uhgrnbgr0nb  29682  cplgrop  29765  wlkl1loop  29965  uspgr2wlkeq  29973  upgrwlkdvdelem  30063  uhgrwkspthlem2  30081  pthdlem2lem  30094  uspgrn2crct  30135  wlkiswwlks2lem3  30198  wlkiswwlks2  30202  wlkiswwlksupgr2  30204  wlklnwwlkln2lem  30209  wwlksnext  30220  wwlksnextfun  30225  rusgrnumwwlk  30305  clwlkclwwlklem2a4  30326  clwlkclwwlklem3  30330  erclwwlksym  30350  erclwwlknsym  30399  eleclclwwlkn  30405  clwwlknonwwlknonb  30435  upgr3v3e3cycl  30509  upgr4cycl4dv4e  30514  conngrv2edg  30524  eupth2lem3lem6  30562  frgrncvvdeqlem8  30635  frgrwopreglem4a  30639  frgrreggt1  30722  frgrreg  30723  grpoinveu  30849  ococss  31623  shmodsi  31719  h1datomi  31911  hoaddsub  32146  adjmul  32422  chjatom  32687  atomli  32712  atcvat4i  32727  mdsymlem3  32735  mdsymlem5  32737  mdsymlem6  32738  sumdmdlem  32748  cdj3lem2a  32766  cdj3lem3a  32769  bnj1204  35378  fineqvinfep  35516  umgr2cycllem  35610  umgr2cycl  35611  cvmsdisj  35740  satfv0fun  35841  satffunlem  35871  satffunlem1lem2  35873  satffunlem2lem2  35876  fundmpss  36237  dfon2lem6  36256  dfon2lem8  36258  ifscgr  36514  lineext  36546  fscgr  36550  idinside  36554  btwnconn1lem11  36567  btwnconn1lem12  36568  btwnconn3  36573  brsegle  36578  seglecgr12  36581  hilbert1.2  36625  exp5d  36792  exp5k  36794  nn0prpwlem  36811  mh-inf3f1  37030  bj-restb  37714  exrecfnlem  38003  poimirlem26  38275  poimirlem29  38278  poimirlem32  38281  areacirc  38342  heibor1lem  38438  pridl  38666  pridlc  38700  dmnnzd  38704  disjlem17  39529  membpartlem19  39541  prtlem11  39618  prtlem17  39628  ax12indn  39695  atcvrj0  40180  cvrat4  40195  athgt  40208  lplnexllnN  40316  2llnjN  40319  lvolnle3at  40334  lncmp  40535  paddclN  40594  pexmidlem4N  40725  cdleme17d3  41248  cdleme50trn2  41303  cdlemf2  41314  cdlemf  41315  cdlemj3  41575  cdlemk26b-3  41657  dihord5b  42011  isnacs3  43421  jm2.26  43709  ordnexbtwnsuc  43974  omabs2  44039  naddgeoa  44101  sbiota1  45124  exbir  45168  tratrb  45225  onfrALT  45238  in2an  45297  pwtrrVD  45513  suctrALT2VD  45524  suctrALT2  45525  tratrbVD  45549  trintALTVD  45568  trintALT  45569  or2expropbi  47748  fcoresf1  47783  2reu8i  47827  2reuimp  47829  zm1nn  48016  2ffzoeq  48042  iccpartiltu  48148  iccpartigtl  48149  iccpartgt  48153  iccpartnel  48164  sbcpr  48247  fmtnofac2lem  48297  fmtnofac2  48298  lighneallem2  48335  odd2prm2  48460  stgoldbwt  48518  sbgoldbst  48520  sbgoldbaltlem1  48521  mogoldbb  48527  uhgrimisgrgric  48673  clnbgrgrim  48676  grimedg  48677  gpgedgvtx1  48804  gpgedg2iv  48809  pgnbgreunbgrlem3  48860  pgnbgreunbgrlem6  48866  pgnbgreunbgr  48867  lidldomn1  48973  idomnzd  49088  ply1mulgsumlem1  49143  lincsumcl  49188  ellcoellss  49192  islinindfis  49206  lindslinindsimp1  49214  lindslinindsimp2lem5  49219  lindsrng01  49225  elfzolborelfzop1  49276  rrx2linest  49499  aacllem  50578