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  3204  mob2  3673  reuind  3711  reupick3  4276  elpwunsn  4645  disjiun  5091  sotr2  5593  wefrc  5645  relop  5828  predpoirr  6329  predfrirr  6330  fnun  6645  mpteqb  7005  tpres  7199  fconst5  7204  funfvima  7228  riotaeqimp  7395  dfwe2  7777  limuni3  7852  tfisi  7859  trom  7875  funcnvuni  7933  resf1ext2b  7936  f1oweALT  7973  frxp  8127  poxp  8129  poxp2  8144  poxp3  8151  wfr3g  8321  onfununi  8333  tz7.48lemOLD  8435  oecl  8529  oaordex  8550  oaass  8553  omwordri  8564  odi  8571  omass  8572  omeu  8577  oen0  8579  oewordi  8584  oewordri  8585  nnarcl  8609  nnmass  8617  brinxper  8731  findcard2  9164  rex2dom  9228  dif1ennnALT  9252  unblem1  9268  unblem2  9269  domunfican  9297  marypha1lem  9409  supiso  9452  inf3lem3  9615  epfrs  9716  frr3g  9744  kardenOLD  9941  infxpenlem  10073  iunfictbso  10174  dfac5  10188  dfac2b  10190  kmlem1  10210  kmlem9  10218  infpssrlem3  10364  fin23lem25  10383  fin23lem30  10401  domtriomlem  10501  axdc3lem4  10512  axcclem  10516  zorn2lem7  10561  konigthlem  10634  wunr1om  10785  tskr1om  10833  gruen  10878  grur1a  10885  indpi  10973  genpnmax  11073  prlem934  11099  ltaddpr  11100  ltexprlem7  11108  ltaprlem  11110  axrrecex  11229  axpre-sup  11235  lelttr  11381  dedekind  11454  addlid  11474  nn0lt2  12743  fzind  12778  fnn0ind  12779  btwnz  12783  uzwo  13019  lbzbi  13044  rpnnen1lem5  13090  ledivge1le  13174  xrlelttr  13266  qbtwnre  13310  xrsupsslem  13418  xrinfmsslem  13419  supxrun  13427  elfz1b  13707  elfz0ubfz0  13746  elfzo0z  13816  fzofzim  13824  elfznelfzo  13888  fleqceilz  13974  fsequb  14098  leexp2r  14297  bernneq  14353  fi1uzind  14632  brfi1indALT  14635  swrdnd0  14787  swrdswrdlem  14833  swrdswrd  14834  wrd2ind  14852  swrdccatin1  14854  swrdccatin2  14858  pfxccatin12lem3  14861  repswswrd  14915  cshweqrep  14952  swrd2lsw  15085  2swrd2eqwrdeq  15086  wrdl3s3  15095  s3iunsndisj  15101  cau3lem  15502  climuni  15699  mulcn2  15743  dvdsabseq  16463  divalglem8  16550  ndvdssub  16559  rplpwr  16712  algcvgblem  16732  lcmf  16788  lcmftp  16791  lcmfunsnlem2lem1  16793  lcmfunsnlem2lem2  16794  lcmfdvdsb  16798  lcmfun  16800  euclemma  16869  prmlem1a  17264  setsstruct2  17332  iscatd  17827  initoeu1  18166  initoeu2  18171  termoeu1  18173  plelttr  18496  insubm  18994  grpinveu  19165  cyccom  19398  symgfixelsi  19629  efgred  19942  telgsumfzs  20183  srgmulgass  20423  srgbinom  20437  lspdisjb  21384  mplcoe5lem  22328  cply1mul  22594  coe1fzgsumd  22602  gsummoncoe1  22606  evl1gsumd  22655  cpmatacl  23014  cpmatmcllem  23016  basis2  23249  0ntr  23369  uncmp  23701  1stcrest  23751  txcls  23903  txcnp  23919  tx1stc  23949  fgss2  24173  alexsubALTlem2  24347  alexsubALTlem3  24348  alexsubALTlem4  24349  metcnp3  24839  tngngp3  24955  reconn  25128  iscau4  25580  ellimc3  26179  ulmbdd  26707  ulmcn  26708  sinq12ge0  26819  gausslemma2dlem3  27677  2sq2  27742  2sqreultlem  27756  2sqreunnltlem  27759  sltsleft  28228  sltsright  28229  noseqind  28660  oldfib  28745  expsgt0  28805  bdayfinbndlem1  28835  bdayfin  28855  elreno2  28863  ax5seglem5  29493  ax5seg  29498  uhgrnbgr0nb  29917  cplgrop  30000  wlkl1loop  30200  uspgr2wlkeq  30208  upgrwlkdvdelem  30304  uhgrwkspthlem2  30322  pthdlem2lem  30335  uspgrn2crct  30379  wlkiswwlks2lem3  30442  wlkiswwlks2  30446  wlkiswwlksupgr2  30448  wlklnwwlkln2lem  30453  wwlksnext  30464  wwlksnextfun  30469  rusgrnumwwlk  30549  clwlkclwwlklem2a4  30570  clwlkclwwlklem3  30574  erclwwlksym  30594  erclwwlknsym  30643  eleclclwwlkn  30649  clwwlknonwwlknonb  30679  umgr2cycllem  30728  umgr2cycl  30729  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  conngrv2edg  30778  eupth2lem3lem6  30816  frgrncvvdeqlem8  30889  frgrwopreglem4a  30893  frgrreggt1  30976  frgrreg  30977  grpoinveu  31103  ococss  31877  shmodsi  31973  h1datomi  32165  hoaddsub  32400  adjmul  32676  chjatom  32941  atomli  32966  atcvat4i  32981  mdsymlem3  32989  mdsymlem5  32991  mdsymlem6  32992  sumdmdlem  33002  cdj3lem2a  33020  cdj3lem3a  33023  bnj1204  35625  fineqvinfep  35766  cvmsdisj  36004  satfv0fun  36105  satffunlem  36135  satffunlem1lem2  36137  satffunlem2lem2  36140  fundmpss  36501  dfon2lem6  36520  dfon2lem8  36522  ifscgr  36779  lineext  36811  fscgr  36815  idinside  36819  btwnconn1lem11  36832  btwnconn1lem12  36833  btwnconn3  36838  brsegle  36843  seglecgr12  36846  hilbert1.2  36890  exp5d  37061  exp5k  37063  nn0prpwlem  37080  mh-inf3f1  37299  bj-restb  37983  exrecfnlem  38270  poimirlem26  38532  poimirlem29  38535  poimirlem32  38538  areacirc  38599  heibor1lem  38711  pridl  38939  pridlc  38973  dmnnzd  38977  disjlem17  39802  membpartlem19  39814  prtlem11  39891  prtlem17  39901  ax12indn  39968  atcvrj0  40453  cvrat4  40468  athgt  40481  lplnexllnN  40589  2llnjN  40592  lvolnle3at  40607  lncmp  40808  paddclN  40867  pexmidlem4N  40998  cdleme17d3  41521  cdleme50trn2  41576  cdlemf2  41587  cdlemf  41588  cdlemj3  41848  cdlemk26b-3  41930  dihord5b  42284  isnacs3  43674  jm2.26  43962  ordnexbtwnsuc  44227  omabs2  44292  naddgeoa  44354  sbiota1  45377  exbir  45421  tratrb  45478  onfrALT  45491  in2an  45550  pwtrrVD  45766  suctrALT2VD  45777  suctrALT2  45778  tratrbVD  45802  trintALTVD  45821  trintALT  45822  or2expropbi  48048  fcoresf1  48083  2reu8i  48127  2reuimp  48129  zm1nn  48316  2ffzoeq  48342  iccpartiltu  48448  iccpartigtl  48449  iccpartgt  48453  iccpartnel  48464  sbcpr  48547  fmtnofac2lem  48597  fmtnofac2  48598  lighneallem2  48635  odd2prm2  48760  stgoldbwt  48818  sbgoldbst  48820  sbgoldbaltlem1  48821  mogoldbb  48827  uhgrimisgrgric  48973  clnbgrgrim  48976  grimedg  48977  gpgedgvtx1  49104  gpgedg2iv  49109  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem6  49166  pgnbgreunbgr  49167  lidldomn1  49272  idomnzd  49387  ply1mulgsumlem1  49442  lincsumcl  49487  ellcoellss  49491  islinindfis  49505  lindslinindsimp1  49513  lindslinindsimp2lem5  49518  lindsrng01  49524  elfzolborelfzop1  49575  rrx2linest  49798  aacllem  50883