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  3207  mob2  3676  reuind  3714  reupick3  4278  elpwunsn  4645  disjiun  5094  sotr2  5597  wefrc  5649  relop  5834  predpoirr  6354  predfrirr  6355  fnun  6675  mpteqb  7036  tpres  7230  fconst5  7235  funfvima  7259  riotaeqimp  7426  dfwe2  7812  limuni3  7887  tfisi  7894  trom  7910  funcnvuni  7968  resf1ext2b  7971  f1oweALT  8008  frxp  8165  poxp  8167  poxp2  8187  poxp3  8194  wfr3g  8365  onfununi  8377  tz7.48lemOLD  8479  oecl  8573  oaordex  8594  oaass  8597  omwordri  8608  odi  8615  omass  8616  omeu  8621  oen0  8623  oewordi  8628  oewordri  8629  nnarcl  8653  nnmass  8661  brinxper  8775  findcard2  9208  rex2dom  9272  dif1ennnALT  9296  unblem1  9312  unblem2  9313  domunfican  9341  marypha1lem  9452  supiso  9495  inf3lem3  9658  epfrs  9759  frr3g  9787  kardenOLD  9987  infxpenlem  10119  iunfictbso  10220  dfac5  10234  dfac2b  10236  kmlem1  10256  kmlem9  10264  infpssrlem3  10410  fin23lem25  10429  fin23lem30  10447  domtriomlem  10547  axdc3lem4  10558  axcclem  10562  zorn2lem7  10607  konigthlem  10680  wunr1om  10831  tskr1om  10879  gruen  10924  grur1a  10931  indpi  11019  genpnmax  11119  prlem934  11145  ltaddpr  11146  ltexprlem7  11154  ltaprlem  11156  axrrecex  11275  axpre-sup  11281  lelttr  11427  dedekind  11500  addlid  11520  nn0lt2  12789  fzind  12824  fnn0ind  12825  btwnz  12829  uzwo  13065  lbzbi  13090  rpnnen1lem5  13136  ledivge1le  13220  xrlelttr  13312  qbtwnre  13356  xrsupsslem  13464  xrinfmsslem  13465  supxrun  13473  elfz1b  13754  elfz0ubfz0  13793  elfzo0z  13863  fzofzim  13871  elfznelfzo  13935  fleqceilz  14021  fsequb  14145  leexp2r  14344  bernneq  14400  fi1uzind  14679  brfi1indALT  14682  swrdnd0  14835  swrdswrdlem  14881  swrdswrd  14882  wrd2ind  14900  swrdccatin1  14902  swrdccatin2  14906  pfxccatin12lem3  14909  repswswrd  14963  cshweqrep  15000  swrd2lsw  15134  2swrd2eqwrdeq  15135  wrdl3s3  15144  s3iunsndisj  15150  cau3lem  15551  climuni  15748  mulcn2  15792  dvdsabseq  16512  divalglem8  16599  ndvdssub  16608  rplpwr  16761  algcvgblem  16781  lcmf  16837  lcmftp  16840  lcmfunsnlem2lem1  16842  lcmfunsnlem2lem2  16843  lcmfdvdsb  16847  lcmfun  16849  euclemma  16918  prmlem1a  17313  setsstruct2  17381  iscatd  17876  initoeu1  18215  initoeu2  18220  termoeu1  18222  plelttr  18545  insubm  19043  grpinveu  19214  cyccom  19447  symgfixelsi  19679  efgred  19992  telgsumfzs  20233  srgmulgass  20473  srgbinom  20487  lspdisjb  21434  mplcoe5lem  22378  cply1mul  22644  coe1fzgsumd  22652  gsummoncoe1  22656  evl1gsumd  22705  cpmatacl  23064  cpmatmcllem  23066  basis2  23299  0ntr  23419  uncmp  23751  1stcrest  23801  txcls  23953  txcnp  23969  tx1stc  23999  fgss2  24223  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALTlem4  24399  metcnp3  24889  tngngp3  25005  reconn  25178  iscau4  25630  ellimc3  26229  ulmbdd  26755  ulmcn  26756  sinq12ge0  26867  gausslemma2dlem3  27725  2sq2  27790  2sqreultlem  27804  2sqreunnltlem  27807  sltsleft  28276  sltsright  28277  noseqind  28708  oldfib  28793  expsgt0  28853  bdayfinbndlem1  28883  bdayfin  28903  elreno2  28911  ax5seglem5  29541  ax5seg  29546  uhgrnbgr0nb  29965  cplgrop  30048  wlkl1loop  30248  uspgr2wlkeq  30256  upgrwlkdvdelem  30352  uhgrwkspthlem2  30370  pthdlem2lem  30383  uspgrn2crct  30427  wlkiswwlks2lem3  30490  wlkiswwlks2  30494  wlkiswwlksupgr2  30496  wlklnwwlkln2lem  30501  wwlksnext  30512  wwlksnextfun  30517  rusgrnumwwlk  30597  clwlkclwwlklem2a4  30618  clwlkclwwlklem3  30622  erclwwlksym  30642  erclwwlknsym  30691  eleclclwwlkn  30697  clwwlknonwwlknonb  30727  umgr2cycllem  30776  umgr2cycl  30777  upgr3v3e3cycl  30811  upgr4cycl4dv4e  30816  conngrv2edg  30826  eupth2lem3lem6  30864  frgrncvvdeqlem8  30937  frgrwopreglem4a  30941  frgrreggt1  31024  frgrreg  31025  grpoinveu  31151  ococss  31925  shmodsi  32021  h1datomi  32213  hoaddsub  32448  adjmul  32724  chjatom  32989  atomli  33014  atcvat4i  33029  mdsymlem3  33037  mdsymlem5  33039  mdsymlem6  33040  sumdmdlem  33050  cdj3lem2a  33068  cdj3lem3a  33071  bnj1204  35712  rmo6  35780  fineqvinfep  35893  cvmsdisj  36202  satfv0fun  36303  satffunlem  36333  satffunlem1lem2  36335  satffunlem2lem2  36338  fundmpss  36710  dfon2lem6  36728  dfon2lem8  36730  ifscgr  36987  lineext  37019  fscgr  37023  idinside  37027  btwnconn1lem11  37040  btwnconn1lem12  37041  btwnconn3  37046  brsegle  37051  seglecgr12  37054  hilbert1.2  37098  exp5d  37269  exp5k  37271  nn0prpwlem  37288  mh-inf3f1  37507  bj-restb  38206  exrecfnlem  38494  poimirlem26  38756  poimirlem29  38759  poimirlem32  38762  areacirc  38823  heibor1lem  38935  pridl  39163  pridlc  39197  dmnnzd  39201  disjlem17  40026  membpartlem19  40038  prtlem11  40115  prtlem17  40125  ax12indn  40192  atcvrj0  40677  cvrat4  40692  athgt  40705  lplnexllnN  40813  2llnjN  40816  lvolnle3at  40831  lncmp  41032  paddclN  41091  pexmidlem4N  41222  cdleme17d3  41745  cdleme50trn2  41800  cdlemf2  41811  cdlemf  41812  cdlemj3  42072  cdlemk26b-3  42154  dihord5b  42508  isnacs3  43914  jm2.26  44202  ordnexbtwnsuc  44461  omabs2  44526  naddgeoa  44588  sbiota1  45609  exbir  45653  tratrb  45710  onfrALT  45723  in2an  45782  pwtrrVD  45998  suctrALT2VD  46009  suctrALT2  46010  tratrbVD  46034  trintALTVD  46053  trintALT  46054  cocanss2  46114  or2expropbi  48309  fcoresf1  48344  2reu8i  48389  2reuimp  48391  zm1nn  48577  2ffzoeq  48603  iccpartiltu  48709  iccpartigtl  48710  iccpartgt  48714  iccpartnel  48725  sbcpr  48808  fmtnofac2lem  48858  fmtnofac2  48859  lighneallem2  48896  odd2prm2  49021  stgoldbwt  49079  sbgoldbst  49081  sbgoldbaltlem1  49082  mogoldbb  49088  uhgrimisgrgric  49234  clnbgrgrim  49237  grimedg  49238  gpgedgvtx1  49365  gpgedg2iv  49370  pgnbgreunbgrlem3  49421  pgnbgreunbgrlem6  49427  pgnbgreunbgr  49428  lidldomn1  49533  idomnzd  49648  ply1mulgsumlem1  49703  lincsumcl  49748  ellcoellss  49752  islinindfis  49766  lindslinindsimp1  49774  lindslinindsimp2lem5  49779  lindsrng01  49785  elfzolborelfzop1  49836  rrx2linest  50059  aacllem  51219