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  1368  mp3an3  1452  3gencl  3480  vtocl3gaf  3532  vtocl3ga  3534  moi  3672  disji  5071  disjord  5075  3optocl  5708  sossfld  6128  f1oresrab  7055  f1cdmsn  7211  soisores  7256  isomin  7266  isofrlem  7269  ovmpos  7489  ov2gf  7490  ndmovord  7531  nnsuc  7809  poxp  8053  frpoins3xp3g  8066  brtpos  8160  dfsmo2  8262  smoiun  8276  smoord  8280  smogt  8282  omeulem1  8492  omeu  8495  oewordi  8501  uniinqs  8716  mapvalg  8755  pmvalg  8756  elmapg  8758  xpdom3  8983  mapdom3  9057  sdomdomtrfi  9105  domsdomtrfi  9106  php  9111  php3  9113  nndomog  9117  onomeneq  9118  sucdom  9123  unxpdomlem3  9137  isinf  9144  f1finf1o  9152  isfinite2  9177  prfi  9203  ordiso  9397  cnfcom3clem  9590  r111  9663  tskwe  9838  pr2ne  9891  infxpenlem  9899  dfac8alem  9915  infdif  10094  infdif2  10095  cff1  10144  coflim  10147  cfslbn  10153  cfslb2n  10154  cofsmo  10155  cfsmolem  10156  cfcoflem  10158  fin23lem27  10214  isf32lem9  10247  isf34lem6  10266  axcc2lem  10322  domtriomlem  10328  axdc4lem  10341  zorn2lem2  10383  axdclem2  10406  konigthlem  10454  gchen1  10511  gchen2  10512  gchpwdom  10556  gchaleph  10557  winainflem  10579  tskcard  10667  gruiun  10685  gruen  10698  intgru  10700  grudomon  10703  grur1a  10705  grutsk1  10707  nqereu  10815  nqereq  10821  ltsonq  10855  prlem934  10919  reclem3pr  10935  1re  11107  axsup  11183  addlid  11291  recex  11744  lemul1a  11970  lt2msq  12002  fimaxre2  12062  zdiv  12538  zextlt  12542  prime  12549  uzind2  12561  fzind  12566  lbzbi  12829  qbtwnxr  13094  qextltlem  13096  xralrple  13099  xltneg  13111  xlt2add  13154  supxrgtmnf  13223  ixxub  13261  ixxlb  13262  ioo0  13265  ico0  13286  ioc0  13287  icc0  13288  iocssre  13322  icossre  13323  iccssre  13324  fzen  13436  expclzlem  13985  expaddz  14008  expmulz  14010  hashgadd  14279  hashunsngx  14295  hashgt23el  14326  elovmpowrd  14460  pfxnd0  14591  ccatopth2  14619  pfxccatin12  14635  cshf1  14712  shftuz  14971  cau3lem  15257  caubnd  15261  climuni  15454  lo1resb  15466  o1resb  15468  o1of2  15515  o1add  15516  o1mul  15517  o1sub  15518  ntrivcvgmul  15804  eflt  16021  moddvds  16169  dvdscmulr  16190  dvdsmulcr  16191  dvdsle  16216  divalglem8  16306  divalgb  16310  ndvdssub  16315  bitsfzo  16341  gcdcllem1  16405  gcdcllem3  16407  dvdsgcd  16450  nn0rppwr  16467  nn0expgcd  16470  lcmgcdlem  16512  lcmfeq0b  16536  qredeu  16564  isprm3  16589  prmdvdsexpr  16623  prmexpb  16625  eulerthlem2  16688  fermltl  16690  coprimeprodsq  16715  pythagtrip  16741  pcprendvds  16747  pcpremul  16750  pcdvdsb  16776  pc2dvds  16786  4sqlem12  16863  4sqlem18  16869  vdwlem10  16897  cshwshashlem3  17004  xpsrnbas  17470  ismred  17499  mrieqv2d  17540  iscatd  17574  isfuncd  17767  fthestrcsetc  18051  fthsetcestrc  18066  poslubd  18312  dirtr  18503  mulgaddcom  19006  ghmrn  19136  pmtrprfv3  19361  mndodcongi  19450  oddvdsnn0  19451  oddvds  19454  odcl2  19472  odhash3  19483  gexdvds  19491  pgpfi  19512  lsmss1b  19573  lsmss2b  19575  efgsrel  19641  efgred  19655  cntzcmn  19747  cyggenod  19791  lt6abl  19802  gsumcom2  19882  pgpfac1lem2  19984  pgpfac1lem3  19986  dvdsunit  20292  unitmulclb  20294  irredrmul  20340  isabvd  20722  lmodvsdi  20813  lss0cl  20875  islbs3  21087  lbsextlem2  21091  xrsdsreclblem  21344  psrbaglefi  21858  mvrf1  21918  coe1fzgsumd  22214  gsummoncoe1  22218  evl1gsumd  22267  scmataddcl  22426  scmatsubcl  22427  mdetunilem9  22530  mdetuni0  22531  mdetmul  22533  m2cpmrngiso  22668  pm2mpf1  22709  opnnei  23030  neindisj2  23033  cncls2  23183  cncls  23184  cnntr  23185  cnpresti  23198  cnprest  23199  lmcnp  23214  isreg2  23287  ordthauslem  23293  unconn  23339  2ndc1stc  23361  kgen2ss  23465  ptclsg  23525  cnmptcom  23588  kqfvima  23640  hmeof1o  23674  fbncp  23749  fbfinnfr  23751  trfbas2  23753  isufil2  23818  ufprim  23819  trufil  23820  filufint  23830  hausflim  23891  flimrest  23893  flimcls  23895  cnpfcf  23951  alexsubALT  23961  tmdgsum  24005  opnsubg  24018  cldsubg  24021  qustgpopn  24030  tsmsxp  24065  blpnf  24307  blssps  24334  blss  24335  blssec  24345  neibl  24411  prdsxmslem2  24439  xrsmopn  24723  metnrm  24773  climcncf  24815  iccpnfhmeo  24865  xrhmeo  24866  bndth  24879  cphsqrtcl3  25109  iscau2  25199  iscmet3lem2  25214  bcthlem5  25250  bcth3  25253  ishl2  25292  ivthlem1  25374  cmmbl  25457  iundisj2  25472  voliunlem2  25474  mbfaddlem  25583  itg2itg1  25659  itg2seq  25665  itg2mulclem  25669  cnplimc  25810  dvres2  25835  deg1nn0clb  26017  deg1lt0  26018  deg1ge  26025  plypf1  26139  plyadd  26144  plymul  26145  coeeu  26152  dgrub2  26162  coeidlem  26164  coeid3  26167  coemullem  26177  coe11  26180  coemulhi  26181  coemulc  26182  dgreq0  26193  dgrlt  26194  dgradd2  26196  vieta1lem2  26241  tanord1  26468  tanord  26469  logccne0  26509  cxpeq0  26609  cxpmul2z  26622  cxpcn3lem  26679  rtprmirr  26692  relogbzcl  26706  angpieqvd  26763  o1cxp  26907  scvxcvx  26918  chtublem  27144  bposlem3  27219  lgsqr  27284  2sqnn  27372  dchrisumlema  27421  dchrisumlem2  27423  ostth2lem3  27568  nosepon  27599  noextenddif  27602  nolesgn2o  27605  nogesgn1o  27607  nosepne  27614  nodense  27626  onnolt  28198  onslt  28199  onsiso  28200  bdayn0p1  28289  bdayn0sf1o  28290  tghilberti2  28611  inagswap  28814  f1otrg  28844  brbtwn2  28878  axpasch  28914  axcontlem4  28940  axcontlem5  28941  upgredg2vtx  29114  usgredg2vtxeuALT  29195  sizusglecusg  29437  upgredginwlk  29609  frgrwopreg1  30290  frgrwopreg2  30291  frgrregorufrg  30298  lpni  30452  ipasslem5  30807  htthlem  30889  omlsii  31375  spansni  31529  spansneleq  31542  elspansn4  31545  sumspansn  31621  homco1  31773  homulass  31774  mdsl0  32282  ssdmd1  32285  ssdmd2  32286  cvdmd  32309  chirredlem2  32363  atdmd  32370  atmd2  32372  disjif  32550  iundisj2f  32562  isoun  32675  preiman0  32683  padct  32693  iocinioc2  32754  iundisj2fi  32771  sgn3da  32809  sgnnbi  32813  sgnpbi  32814  indpi1  32833  archiabllem1a  33152  archiabllem2a  33155  slmdvsdi  33176  ordtconnlem1  33929  measinblem  34225  measres  34227  measdivcstALTV  34230  mbfmco2  34270  orvclteinc  34481  bnj605  34911  bnj607  34920  bnj964  34947  bnj1033  34973  bnj1128  34994  bnj1137  34999  bnj1136  35001  bnj1413  35039  bnj60  35066  rankfilimb  35105  r1filim  35107  fineqvac  35131  fineqvnttrclselem3  35135  fineqvnttrclse  35136  cusgredgex  35158  subgrwlk  35168  acycgr1v  35185  cvmlift2lem10  35348  msubvrs  35596  wsuclem  35859  dfrdg4  35985  brcolinear2  36092  brsegle2  36143  nn0prpw  36357  ntruni  36361  clsint2  36363  fnessref  36391  fnemeet2  36401  fnejoin2  36403  limsucncmpi  36479  ee7.2aOLD  36495  bj-idreseq  37196  dissneqlem  37374  isbasisrelowllem1  37389  isbasisrelowllem2  37390  icoreclin  37391  poimirlem9  37669  poimirlem30  37690  poimirlem32  37692  areacirc  37753  filbcmb  37780  mettrifi  37797  heiborlem8  37858  heiborlem10  37860  heibor  37861  riscer  38028  igenval2  38106  lshpcmp  39027  eqlkr  39138  lkrlsp2  39142  lkrshp  39144  cvrnbtwn2  39314  cvlexch3  39371  cvlexch4N  39372  cvlatexchb1  39373  cvlsupr3  39383  exatleN  39443  cvratlem  39460  atcvrj2b  39471  cvrat3  39481  cvrat4  39482  athgt  39495  ps-1  39516  ps-2  39517  3atlem5  39526  3at  39529  llnneat  39553  llnmlplnN  39578  lplnneat  39584  lplnnelln  39585  islpln2a  39587  lplnriaN  39589  lplnribN  39590  lplnexllnN  39603  2llnjaN  39605  lvolnle3at  39621  lvolneatN  39627  lvolnelln  39628  lvolnelpln  39629  islvol2aN  39631  dalem62  39773  pmapglb2N  39810  pmapglb2xN  39811  lncmp  39822  paddasslem14  39872  paddasslem15  39873  pmod2iN  39888  hlmod1i  39895  pclfinclN  39989  osumcllem8N  40002  pexmidlem4N  40012  pl42lem1N  40018  pl42lem4N  40021  lhpexle1  40047  lhpexle2lem  40048  lhpmcvr5N  40066  lhpmcvr6N  40067  ltrneq  40188  trlnidatb  40216  cdleme0ex2N  40263  cdleme27a  40406  cdleme17d3  40535  cdlemeg46gfre  40571  cdleme48gfv1  40575  cdlemeg49lebilem  40578  cdlemf2  40601  cdlemf  40602  cdlemfnid  40603  trlord  40608  cdlemg31c  40738  cdlemg35  40752  trlcone  40767  tendoeq2  40813  cdlemj3  40862  cdlemk26b-3  40944  cdlemk33N  40948  cdleml3N  41017  cdlemn  41251  dih1dimb2  41280  dihord5apre  41301  dihmeetlem1N  41329  dihglblem5apreN  41330  dihglblem2N  41333  dihglblem3N  41334  dihmeetlem13N  41358  dihmeetlem15N  41360  dihatexv  41377  hdmap14lem12  41918  uzindd  42010  lcmineqlem1  42062  sticksstones1  42179  dvdsexpnn0  42367  frlmfzowrdb  42537  oddcomabszz  42977  jm2.19lem4  43025  fiuneneq  43225  idomsubgmo  43226  omcl2  43366  pwinfi3  43596  gneispa  44163  mnringmulrcld  44261  grumnudlem  44318  ismnushort  44334  binomcxplemnn0  44382  addrcom  44507  int3  44645  suctrALT  44858  suctrALTcf  44954  suctrALT3  44956  chordthmALT  44965  iunconnlem2  44967  relpmin  44985  relpfrlem  44986  stoweidlem26  46064  stoweidlem34  46072  issald  46371  goldbachth  47578  grlimgrtri  48034  nnsgrp  48208  ply1mulgsumlem1  48418  lubsscl  48991  glbsscl  48992