Theorem 3expia 1121

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

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

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant125  1367  mp3an3  1451  3gencl  3509  vtocl3gaf  3565  vtocl3ga  3567  moi  3708  disji  5110  disjord  5114  3optocl  5764  sossfld  6188  f1oresrab  7128  f1cdmsn  7285  soisores  7330  isomin  7340  isofrlem  7343  ovmpos  7564  ov2gf  7565  ndmovord  7606  nnsuc  7888  poxp  8136  frpoins3xp3g  8149  brtpos  8243  dfsmo2  8370  smoiun  8384  smoord  8388  smogt  8390  omeulem1  8603  omeu  8606  oewordi  8612  uniinqs  8820  mapvalg  8859  pmvalg  8860  elmapg  8862  xpdom3  9093  mapdom3  9172  sdomdomtrfi  9224  domsdomtrfi  9225  php  9230  php3  9232  nndomog  9236  php3OLD  9244  onomeneq  9248  sucdom  9254  unxpdomlem3  9271  isinf  9279  isinfOLD  9280  f1finf1o  9288  isfinite2  9317  prfi  9346  ordiso  9539  cnfcom3clem  9728  r111  9798  tskwe  9973  pr2ne  10027  pr2neOLD  10028  infxpenlem  10036  dfac8alem  10052  infdif  10231  infdif2  10232  cff1  10281  coflim  10284  cfslbn  10290  cfslb2n  10291  cofsmo  10292  cfsmolem  10293  cfcoflem  10295  fin23lem27  10351  isf32lem9  10384  isf34lem6  10403  axcc2lem  10459  domtriomlem  10465  axdc4lem  10478  zorn2lem2  10520  axdclem2  10543  konigthlem  10591  gchen1  10648  gchen2  10649  gchpwdom  10693  gchaleph  10694  winainflem  10716  tskcard  10804  gruiun  10822  gruen  10835  intgru  10837  grudomon  10840  grur1a  10842  grutsk1  10844  nqereu  10952  nqereq  10958  ltsonq  10992  prlem934  11056  reclem3pr  11072  1re  11244  axsup  11319  addlid  11427  recex  11878  lemul1a  12104  lt2msq  12136  fimaxre2  12196  zdiv  12672  zextlt  12676  prime  12683  uzind2  12695  fzind  12700  lbzbi  12961  qbtwnxr  13225  qextltlem  13227  xralrple  13230  xltneg  13242  xlt2add  13285  supxrgtmnf  13354  ixxub  13391  ixxlb  13392  ioo0  13395  ico0  13416  ioc0  13417  icc0  13418  iocssre  13450  icossre  13451  iccssre  13452  fzen  13564  expclzlem  14107  expaddz  14130  expmulz  14132  hashgadd  14399  hashunsngx  14415  hashgt23el  14446  elovmpowrd  14579  pfxnd0  14709  ccatopth2  14738  pfxccatin12  14754  cshf1  14831  shftuz  15091  cau3lem  15376  caubnd  15380  climuni  15571  lo1resb  15583  o1resb  15585  o1of2  15632  o1add  15633  o1mul  15634  o1sub  15635  ntrivcvgmul  15921  eflt  16136  moddvds  16284  dvdscmulr  16305  dvdsmulcr  16306  dvdsle  16330  divalglem8  16420  divalgb  16424  ndvdssub  16429  bitsfzo  16455  gcdcllem1  16519  gcdcllem3  16521  dvdsgcd  16564  nn0rppwr  16581  nn0expgcd  16584  lcmgcdlem  16626  lcmfeq0b  16650  qredeu  16678  isprm3  16703  prmdvdsexpr  16737  prmexpb  16739  eulerthlem2  16802  fermltl  16804  coprimeprodsq  16829  pythagtrip  16855  pcprendvds  16861  pcpremul  16864  pcdvdsb  16890  pc2dvds  16900  4sqlem12  16977  4sqlem18  16983  vdwlem10  17011  cshwshashlem3  17118  xpsrnbas  17592  ismred  17621  mrieqv2d  17658  iscatd  17692  isfuncd  17886  fthestrcsetc  18170  fthsetcestrc  18185  poslubd  18432  dirtr  18621  mulgaddcom  19090  ghmrn  19221  pmtrprfv3  19445  mndodcongi  19534  oddvdsnn0  19535  oddvds  19538  odcl2  19556  odhash3  19567  gexdvds  19575  pgpfi  19596  lsmss1b  19657  lsmss2b  19659  efgsrel  19725  efgred  19739  cntzcmn  19831  cyggenod  19875  lt6abl  19886  gsumcom2  19966  pgpfac1lem2  20068  pgpfac1lem3  20070  dvdsunit  20352  unitmulclb  20354  irredrmul  20400  isabvd  20786  lmodvsdi  20856  lss0cl  20918  islbs3  21130  lbsextlem2  21134  xrsdsreclblem  21397  psrbaglefi  21913  mvrf1  21973  coe1fzgsumd  22275  gsummoncoe1  22279  evl1gsumd  22328  scmataddcl  22489  scmatsubcl  22490  mdetunilem9  22593  mdetuni0  22594  mdetmul  22596  m2cpmrngiso  22731  pm2mpf1  22772  opnnei  23093  neindisj2  23096  cncls2  23246  cncls  23247  cnntr  23248  cnpresti  23261  cnprest  23262  lmcnp  23277  isreg2  23350  ordthauslem  23356  unconn  23402  2ndc1stc  23424  kgen2ss  23528  ptclsg  23588  cnmptcom  23651  kqfvima  23703  hmeof1o  23737  fbncp  23812  fbfinnfr  23814  trfbas2  23816  isufil2  23881  ufprim  23882  trufil  23883  filufint  23893  hausflim  23954  flimrest  23956  flimcls  23958  cnpfcf  24014  alexsubALT  24024  tmdgsum  24068  opnsubg  24081  cldsubg  24084  qustgpopn  24093  tsmsxp  24128  blpnf  24371  blssps  24398  blss  24399  blssec  24409  neibl  24477  prdsxmslem2  24505  xrsmopn  24789  metnrm  24839  climcncf  24881  iccpnfhmeo  24931  xrhmeo  24932  bndth  24945  cphsqrtcl3  25176  iscau2  25266  iscmet3lem2  25281  bcthlem5  25317  bcth3  25320  ishl2  25359  ivthlem1  25441  cmmbl  25524  iundisj2  25539  voliunlem2  25541  mbfaddlem  25650  itg2itg1  25726  itg2seq  25732  itg2mulclem  25736  cnplimc  25877  dvres2  25902  deg1nn0clb  26084  deg1lt0  26085  deg1ge  26092  plypf1  26206  plyadd  26211  plymul  26212  coeeu  26219  dgrub2  26229  coeidlem  26231  coeid3  26234  coemullem  26244  coe11  26247  coemulhi  26248  coemulc  26249  dgreq0  26260  dgrlt  26261  dgradd2  26263  vieta1lem2  26308  tanord1  26534  tanord  26535  logccne0  26575  cxpeq0  26675  cxpmul2z  26688  cxpcn3lem  26745  rtprmirr  26758  relogbzcl  26772  angpieqvd  26829  o1cxp  26973  scvxcvx  26984  chtublem  27210  bposlem3  27285  lgsqr  27350  2sqnn  27438  dchrisumlema  27487  dchrisumlem2  27489  ostth2lem3  27634  nosepon  27665  noextenddif  27668  nolesgn2o  27671  nogesgn1o  27673  nosepne  27680  nodense  27692  tghilberti2  28601  inagswap  28804  f1otrg  28834  brbtwn2  28869  axpasch  28905  axcontlem4  28931  axcontlem5  28932  upgredg2vtx  29105  usgredg2vtxeuALT  29186  sizusglecusg  29428  upgredginwlk  29601  frgrwopreg1  30284  frgrwopreg2  30285  frgrregorufrg  30292  lpni  30446  ipasslem5  30801  htthlem  30883  omlsii  31369  spansni  31523  spansneleq  31536  elspansn4  31539  sumspansn  31615  homco1  31767  homulass  31768  mdsl0  32276  ssdmd1  32279  ssdmd2  32280  cvdmd  32303  chirredlem2  32357  atdmd  32364  atmd2  32366  disjif  32538  iundisj2f  32550  isoun  32658  preiman0  32666  padct  32678  iocinioc2  32728  iundisj2fi  32746  indpi1  32792  archiabllem1a  33144  archiabllem2a  33147  slmdvsdi  33167  ordtconnlem1  33864  measinblem  34162  measres  34164  measdivcstALTV  34167  mbfmco2  34208  orvclteinc  34419  sgn3da  34485  sgnnbi  34489  sgnpbi  34490  bnj605  34862  bnj607  34871  bnj964  34898  bnj1033  34924  bnj1128  34945  bnj1137  34950  bnj1136  34952  bnj1413  34990  bnj60  35017  fineqvac  35052  cusgredgex  35068  subgrwlk  35078  acycgr1v  35095  cvmlift2lem10  35258  msubvrs  35506  wsuclem  35767  dfrdg4  35893  brcolinear2  36000  brsegle2  36051  nn0prpw  36265  ntruni  36269  clsint2  36271  fnessref  36299  fnemeet2  36309  fnejoin2  36311  limsucncmpi  36387  ee7.2aOLD  36403  bj-idreseq  37104  dissneqlem  37282  isbasisrelowllem1  37297  isbasisrelowllem2  37298  icoreclin  37299  poimirlem9  37577  poimirlem30  37598  poimirlem32  37600  areacirc  37661  filbcmb  37688  mettrifi  37705  heiborlem8  37766  heiborlem10  37768  heibor  37769  riscer  37936  igenval2  38014  lshpcmp  38930  eqlkr  39041  lkrlsp2  39045  lkrshp  39047  cvrnbtwn2  39217  cvlexch3  39274  cvlexch4N  39275  cvlatexchb1  39276  cvlsupr3  39286  exatleN  39347  cvratlem  39364  atcvrj2b  39375  cvrat3  39385  cvrat4  39386  athgt  39399  ps-1  39420  ps-2  39421  3atlem5  39430  3at  39433  llnneat  39457  llnmlplnN  39482  lplnneat  39488  lplnnelln  39489  islpln2a  39491  lplnriaN  39493  lplnribN  39494  lplnexllnN  39507  2llnjaN  39509  lvolnle3at  39525  lvolneatN  39531  lvolnelln  39532  lvolnelpln  39533  islvol2aN  39535  dalem62  39677  pmapglb2N  39714  pmapglb2xN  39715  lncmp  39726  paddasslem14  39776  paddasslem15  39777  pmod2iN  39792  hlmod1i  39799  pclfinclN  39893  osumcllem8N  39906  pexmidlem4N  39916  pl42lem1N  39922  pl42lem4N  39925  lhpexle1  39951  lhpexle2lem  39952  lhpmcvr5N  39970  lhpmcvr6N  39971  ltrneq  40092  trlnidatb  40120  cdleme0ex2N  40167  cdleme27a  40310  cdleme17d3  40439  cdlemeg46gfre  40475  cdleme48gfv1  40479  cdlemeg49lebilem  40482  cdlemf2  40505  cdlemf  40506  cdlemfnid  40507  trlord  40512  cdlemg31c  40642  cdlemg35  40656  trlcone  40671  tendoeq2  40717  cdlemj3  40766  cdlemk26b-3  40848  cdlemk33N  40852  cdleml3N  40921  cdlemn  41155  dih1dimb2  41184  dihord5apre  41205  dihmeetlem1N  41233  dihglblem5apreN  41234  dihglblem2N  41237  dihglblem3N  41238  dihmeetlem13N  41262  dihmeetlem15N  41264  dihatexv  41281  hdmap14lem12  41822  uzindd  41919  lcmineqlem1  41971  sticksstones1  42088  metakunt1  42147  metakunt5  42151  dvdsexpnn0  42314  frlmfzowrdb  42459  oddcomabszz  42901  jm2.19lem4  42949  fiuneneq  43149  idomsubgmo  43150  omcl2  43291  pwinfi3  43521  gneispa  44088  mnringmulrcld  44192  grumnudlem  44249  ismnushort  44265  binomcxplemnn0  44313  addrcom  44439  int3  44577  suctrALT  44791  suctrALTcf  44887  suctrALT3  44889  chordthmALT  44898  iunconnlem2  44900  relpmin  44918  relpfrlem  44919  stoweidlem26  45986  stoweidlem34  45994  issald  46293  goldbachth  47480  grlimgrtri  47909  nnsgrp  48039  ply1mulgsumlem1  48249  lubsscl  48805  glbsscl  48806